01 / الحد
أبقِ قاعدة الثقة صغيرة
لا تضع المولدات المعقدة أو الذكاء الاصطناعي في مركز الثقة. اجعل جانب الفحص الصغير واضحًا.
Finite Field / Math Lab
ابنِ دليلًا على الصحة، لا نتائج سريعة فقط.
Math Lab هو المكان الذي نعرض فيه كيف نتعامل مع النمذجة الرياضية وإثبات المبرهنات والتحقق الصوري وقابلية إعادة الإنتاج والتنفيذ الموثوق من دون المبالغة في قوة الدليل.
- مشاريع عامة
- NPA / STD / MATHLIB
- اللغة الأساسية
- Rust
- لقطة NPA
- v0.1.1
تدقيق البرهان / عرض مفاهيمي
قراءة فقط
01 البايتات القياسية / الصيغة تم
02 certificate_hash تم
03 فحص البرهان التابع تم
04 حكم بلا اعتماد على المصدر تم
حد الثقة ظاهر
لا تدعي هذه الصفحة أن NPA بديل عملي عن Lean أو Rocq، ولا تنفذ المحاكاة داخل المتصفح NPA فعليًا.
مبدأ المختبر
انشر النتائج وحدود الفحص معًا.
نتيجة مثل «نجح الأمر» أو «كان سريعًا» أو «ثبت البرهان» لا تكفي. نعرض المدخلات والافتراضات والأجزاء الموثوقة والآثار القابلة للفحص المستقل والقضايا غير المحسومة كلًا على حدة.
02 / الدليل
حوّل الدليل إلى أثر
اترك الشهادات والتجزئات وقوائم الافتراضات وشروط القياس والسجلات بصيغة يستطيع الآخرون فحصها.
03 / إعادة الإنتاج
صمم من أجل قابلية إعادة الإنتاج
ثبّت سلاسل الأدوات وبيانات الإدخال وأوامر التشغيل والمعايير كي يمكن فحص النتيجة مرة أخرى.
04 / الصراحة
لا تبالغ في حالة البحث
اعرض المناهج العملية والتجارب والبحث كلًا على حدة. ضع القيود بجانب النتائج.
مراجعة منهج
فئة منهج خدمة لا تزال تحتاج إلى نطاق ومسؤولية ودليل من العميل وموافقة قبل وصفها بأنها جاهزة للمشروع.
تجريبي
يوجد تنفيذ عامل، لكن الحجم أو التوافق أو الأداء أو مواصفة العمل قد تتغير. يلزم توثيق الإصدار وخطوات إعادة الإنتاج.
بحث
التصميم أو التقييم أو البرهان أو التنفيذ لا يزال جاريًا. هذا لا يعني التوفر التجاري أو الاكتمال.
محفظة البحث
اعرض البحث حسب النضج والآثار.
تعرض كل بطاقة درجة النضج والآثار والحالة الحالية والتحقق التالي. البحث والمرشحات يستخدمان حالة داخل المتصفح فقط.
8 معروضة
تجريبي
مفتوح المصدر
01
Nano Proof Auditor
سلسلة أدوات برهان تبدأ من الشهادة
سلسلة أدوات بحثية تضع شهادات البرهان القياسية وقاعدة فحص صغيرة في مركز مراجعة البراهين التابعة.
- الآثار
- المصدر / المواصفة / قوالب CI
- الحالي
- لقطة عامة v0.1.1
- التحقق التالي
- حزم مبرهنات خارجية وفحص مستقل
تجريبي
مفتوح المصدر
02
مكتبة NPA القياسية
Logic / Nat / List / Algebra
مستودع حزم مبرهنات معيارية لأسس NPA القابلة لإعادة الاستخدام.
- الآثار
- المصدر / حزم البرهان
- الحالي
- مستودع عام منفصل
- التحقق التالي
- نطاق الحزم والتوافق
بحث
مفتوح المصدر
03
مكتبة NPA الرياضية
مكتبة رياضيات صورية
اتجاه مكتبي لتخزين المبرهنات الرياضية كحزم برهان قابلة للفحص المستقل.
- الآثار
- المصدر / حزم البرهان
- الحالي
- مستودع عام قيد التطوير
- التحقق التالي
- بنية المكتبة وتدقيق التبعيات
مراجعة منهج
منهج
04
نماذج التخطيط المقيد
جدولة / مسارات / إسناد
منهج لفصل القيود الصارمة ومقاييس التقييم في أعمال المناوبات والزيارات والمسارات والإنتاج والإسناد.
- الآثار
- نموذج / نموذج أولي / تقرير شرح
- الحالي
- منهج خدمة؛ الادعاء العام محدود بمراجعة المنهج
- التحقق التالي
- دليل العميل واعتماد النطاق
بحث
قياس
05
تقييم قابل لإعادة الإنتاج لمحركات الحل
معيار قياس ودليل
برنامج لتثبيت مجموعات الحالات والعتاد وحدود الوقت والبذور العشوائية والسجلات الخام قبل تقديم ادعاءات الأداء.
- الآثار
- سجل معايير / سجلات خام / تقرير
- الحالي
- تصميم برنامج بحثي
- التحقق التالي
- أول مجموعة معايير عامة
بحث
مناهج صورية
06
التحقق من منطق الأعمال الحرج
ثوابت لأنظمة الأعمال
بحث في فصل الرسوم والصلاحيات والمخزون وانتقالات الحالة إلى مواصفات وثوابت.
- الآثار
- مواصفة / ثوابت / اختبار أو تقرير برهان
- الحالي
- دراسة نطاق
- التحقق التالي
- اختيار حالة إنتاجية محدودة واحدة
تجريبي
هندسة
07
مكونات موثوقة صغيرة في Rust
مكونات موثوقة صغيرة
عمل تنفيذي يبقي الأجزاء الحرجة للثقة مثل المدققات والتجزئات صغيرة بما يكفي للتفتيش.
- الآثار
- نواة NPA / حزمة الشهادات / المدقق المرجعي
- الحالي
- تنفيذ عام داخل NPA
- التحقق التالي
- توافق المدقق المستقل
بحث
ذكاء اصطناعي × برهان
08
مساعدة الذكاء الاصطناعي والفحص المستقل
ولّد بحرية وافحص بصرامة
اتجاه بحثي يضع الذكاء الاصطناعي في توليد المرشحات بينما يُفحص الدليل النهائي بشكل مستقل.
- الآثار
- مولد مرشحات / شهادة / تقرير مدقق
- الحالي
- اتجاه بحثي متسق مع نموذج ثقة NPA
- التحقق التالي
- قياس سير تأليف البرهان
لم يتم العثور على مجال بحث مطابق.
جرّب كلمة مفتاحية أخرى أو أعد مرشح النضج إلى الكل.
Nano Proof Auditor
افصل توليد البرهان عما نثق به.
NPA سلسلة أدوات برهان تبدأ من الشهادة لفحص البراهين التابعة. يمكن للواجهات والتكتيكات والبحث عن المبرهنات والإضافات والذكاء الاصطناعي وملفات المصدر وحالة CI أن تساعد في إنشاء المرشحات، لكنها ليست دليل البرهان الموثوق.
تجريبيمفتوح المصدرApache-2.0
اللقطة الحالية
v0.1.1
تمت مراجعة المعلومات العامة في 2026-06-21.
النواة الأساسية
Rust
مدقق Rust والنواة جزء من جانب الفحص.
أثر التدقيق
.npcert
بايتات الشهادة القياسية هي موضوع الفحص.
نقطة إعادة الفحص
مراجعة يدوية
يجب مراجعة حالة المستودع وظهور الحزم قبل النشر.
مستكشف حدود الثقة
تنقل بين ما نثق به وما لا نثق به.
انقر على كل عقدة لتفحص ما تفعله، وما تنتجه، وما الفحص الذي لا يزال مطلوبًا.
غير موثوق
مفحوص
حد مهم
لا يُعد NPA حاليًا بديلًا عمليًا عن Lean أو Rocq. تشرح هذه الصفحة تصميم البحث المرتكز على الشهادات ولا تضمن أنظمة تجارية بلا أخطاء أو حلًا آليًا للمبرهنات.
فحص الشهادة / محاكاة تفسيرية
اختبر مسار فحص الشهادة.
تشرح تفاعلات المتصفح مسار التفتيش. وهي لا تشغل NPA أو Rust أو WASM أو شهادات برهان حقيقية.
مثال CLI
npa package verify-certs --root . --checker reference --json
NPA / أثر التدقيق
جاهز
- 01 قراءة الشهادةالبايتات القياسية / الصيغة انتظار
- 02 فحص تجزئة الشهادةcertificate_hash انتظار
- 03 الفحص باستخدام النواةفحص البرهان التابع انتظار
- 04 إعادة الفحص بالمدقق المرجعيحكم بلا اعتماد على المصدر انتظار
- 05 مقارنة تقرير البديهياتتجزئة تقرير البديهيات انتظار
الحكم
لم يتم تشغيل الشرح بعد.شغّل الشرح لعرض الخطوات بالترتيب.
منظومة البرهان
وضّح الأدوار بدلًا من ترتيب الأدوات.
Lean وRocq منظومتان ناضجتان لمساعدات البرهان. يُعرض NPA هنا كمشروع بحث وتنفيذ يتمحور حول الشهادات، لا كترتيب بديل أو مقارنة تفاضلية.
| العنصر | Lean | Rocq | NPA |
|---|---|---|---|
| الموضع | لغة برمجة ومساعد برهان مفتوح المصدر. | مبرهن تفاعلي له تاريخ بحثي طويل. | مستودع بحث وتنفيذ للفحص الذي يبدأ من الشهادة. |
| الاستخدام المعتاد | الرياضيات والتحقق من البرمجيات والبرمجة. | الرياضيات والمواصفات والتحقق من البرامج والاستخراج. | بحث في شهادات البرهان والفحص المستقل. |
| التركيز | قابلية التوسعة والمكتبات والبرهان التفاعلي. | التعبيرية والمناهج الناضجة والمكتبات. | قاعدة ثقة صغيرة وشهادات قياسية. |
| كيف تتعامل هذه الصفحة معه | مرجع للتعلم والمقارنة والتشغيل المتبادل. | مرجع للتعلم والمقارنة ومناهج الصياغة الصورية. | مشروع بحث من Finite Field. |
| الحد | لا تزال المعرفة المتخصصة مطلوبة. | لا تزال المعرفة المتخصصة مطلوبة. | ليس مقصودًا حاليًا كبديل عملي عن Lean أو Rocq. |
منهج البحث
حوّل «نجح الأمر» إلى إجراء فحص قابل للتكرار.
تصبح النتيجة أقوى عندما يستطيع شخص آخر إعادة تشغيلها وفحصها ورفضها ضمن الشروط نفسها.
السؤال
حدد ما ينبغي فحصه: الأداء أو الصحة أو التوافق أو النطاق.
الافتراضات
اكتب الافتراضات والاستثناءات والبديهيات وفجوات البيانات والانحياز قبل التقييم.
الأثر
احتفظ بالمصدر والشهادات والمدخلات وسجلات التنفيذ والتجزئات.
فحص مستقل
افحص النتائج عبر مسار مختلف عن جانب التوليد.
معيار قياس
ثبّت العتاد والإصدارات وحدود الوقت ومجموعات الحالات والبذور العشوائية.
الحدود
انشر الإخفاقات والحالات غير المدعومة وحدود الأداء والتحقق التالي.
منشئ قابلية إعادة الإنتاج
افحص ما لا يزال ينقص نشر البحث.
تُعالج القائمة داخل المتصفح فقط. وهي ليست درجة اعتماد.
الجاهزية
0%الإجراء التالي
حدد سؤال البحث وشرط النجاح أولًا.قبل تحديد صيغ الآثار، ثبّت ما سيُقارن أو يُفحص.
آثار عامة
تابع الآثار العامة من مدخل واحد.
تتجنب الصفحة استدعاءات GitHub API وقت التشغيل. حالة المستودعات لقطة تمت مراجعتها ويجب فحصها قبل النشر.
4 أثرًا
finitefield-org
npa
سلسلة أدوات برهان تبدأ من الشهادة
تحقق
package verify-certs
finitefield-org
npa-std
حزمة مبرهنات معيارية
الدور
Std.Logic / Nat / List
finitefield-org
npa-mathlib
مكتبة رياضيات صورية
الدور
حزم مبرهنات صورية
GitHub
finitefield-org
فهرس المستودعات العامة
فهرس
كل المستودعات العامة
لا يوجد أثر عام يطابق البحث.
سياسة النشر
ينبغي أن تحمل المستودعات العامة والملاحظات البحثية ومعايير القياس تاريخ الفحص ودرجة النضج وخطوات إعادة الإنتاج والقيود المعروفة. لا تُعرض النجوم أو أعداد الالتزامات كمؤشرات لجودة البحث.
من المختبر إلى التشغيل
أدخل انضباط البحث في تصميم أنظمة الأعمال.
ليست كل أنظمة العملاء بحاجة إلى إثبات مبرهنات. القيمة العملية هي تحديد ما يجب الوثوق به ومقارنته وفحصه وتصحيحه واعتماده من البشر.
ممارسة المختبر
افصل التوليد والحساب والفحص النهائي بدلًا من الثقة بكل الطبقات بالتساوي.
احتفظ بالمدخلات والمخرجات والشهادات والتجزئات والسجلات كآثار قابلة للمراجعة.
ثبّت البيانات والإصدارات والأوامر ومعايير التقييم قبل مقارنة النتائج.
انشر القيود والحالات الفاشلة والنقاط غير المحسومة بنفس وزن النتائج.
نظام العميل
حدد من يُدخل، ومن يراجع، ومن يتجاوز، ومن يؤكد النتيجة.
اعرض القيود ودرجات التقييم والمرشحين المرفوضين والنقاط غير المحسومة.
احفظ تغييرات الشروط وتشغيلات الحساب وتاريخ الموافقة النهائي.
اجعل المخرجات الآلية قابلة للتصحيح والرفض والشرح للمشغلين.
01
المناوبات وتخطيط الموظفين
اعرض مخالفات القواعد ومدى تلبية التفضيلات كلًا على حدة.
02 تخطيط مسارات المركباتأبقِ أسباب المسار والسعة ونوافذ الوقت والاستثناءات مرئية.
03 جدولة الإنتاجاشرح العمل غير المجدول والاختناقات والمفاضلات في الإعداد.
04 مطابقة الإسناداعرض أسباب المرشحين والبدائل قبل الموافقة.
ملاحظات بحثية
اجعل تاريخ التحديث والأدلة سهلَي القراءة.
ليست كل بطاقة مقالًا منشورًا. تبقى الملاحظات قيد التحضير غير موسومة كعمل منشور حتى تحصل على تواريخ ومصادر وخطوات إعادة إنتاج.
NPA / الحالي
لماذا نضع الشهادات في المركز
لماذا ينبغي أن يكون الدليل النهائي شهادة معيارية يفحصها مسار مستقل صغير.
اعرض المستودع العامملاحظة تصميم / مخططة
جعل نتائج التحسين قابلة للشرح
ملاحظة تصميم حول إظهار الأهداف والقيود الصارمة والتفضيلات المرنة والإسنادات غير المحسومة في واجهة المستخدم.
اعرض العروض ذات الصلةمعيار قياس / مخطط
شروط مقارنة عادلة بين المحركات
ملاحظة مخططة عن مجموعات الحالات وحدود الوقت وفجوات المثالية والبذور العشوائية والعتاد.
اعرض معايير النشرالعناصر «قيد التحضير» ليست مقالات منشورة. بعد النشر تحصل كل ملاحظة على تاريخ ومصدر ومؤلف ومسار إعادة إنتاج وقيود معروفة.
الأسئلة الشائعة
حدود البحث وأدوات البرهان والاستخدام التجاري.
تُوضح هذه النقاط قبل أن تُفهم صفحات البحث على أنها ضمانات إنتاج.
اقرأ عن الشركة01 هل Math Lab خدمة تطوير تعاقدية؟
لا. إنه مكان لنشر موقف البحث وآثاره. في نقاشات العملاء نفصل بين المناهج القابلة للتطبيق، والمناهج التي تحتاج تحققًا أكثر، والموضوعات البحثية.
02 هل يمكن أن يحل NPA محل Lean أو Rocq؟
لا. NPA الحالي ليس بديلًا عمليًا عن Lean أو Rocq. إنه مشروع بحث وتنفيذ حول الشهادات والفحص المستقل وقاعدة الثقة الصغيرة.
03 هل تثقون بالبراهين التي يولدها الذكاء الاصطناعي كما هي؟
لا. يساعد الذكاء الاصطناعي والبحث والتكتيكات في توليد المرشحين. نركز على ما إذا كانت الشهادة النهائية مقبولة لدى مدقق مستقل عن مسارات التوليد.
04 هل يزيل التحقق الصوري كل الأخطاء؟
لا. تفحص المناهج الصورية خصائص محددة مقابل مواصفة صريحة. المواصفات الخاطئة، والكود خارج النطاق، والتشغيل، والخدمات الخارجية تحتاج مراجعة منفصلة.
05 هل يرتبط هذا بعمل أنظمة الأعمال؟
نعم. نطبق هذا الانضباط عادة بالتدرج: القيود، وأسباب النتائج، وتاريخ الحساب، وحدود الصلاحيات، وفحوص منطق الأعمال المهم.
ناقش مشكلة
يمكنك مناقشة العمل المراد حله، لا موضوع البحث فقط.
ابدأ من جدول البيانات الحالي والقواعد والمواضع التي يصحح فيها البشر القرارات. يمكننا فرز ما إذا كانت النمذجة الرياضية أو أتمتة القواعد أو نموذج أولي ينبغي أن يأتي أولًا.
لقطة المصادر / 2026-06-21
تعتمد ادعاءات NPA على لقطة مستودع finitefield-org/npa. ويستند تموضع Lean وRocq إلى موقعيهما الرسميين. تمت مراجعة حالة المستودعات وأحدث الوسوم وصياغة مراجعة المنهج في 2026-06-28.