الحالة العامة
مستودع بحث وتنفيذ
مستودع GitHub عام، لكن هذه الصفحة تصف مستودع بحث وتنفيذ، لا خدمة منشورة.
العودة إلى Math Lab
NPA / فحص برهان يبدأ من الشهادة
NPA: اكشف حد دليل البرهان قبل الوثوق بالنتيجة.
تعيد هذه الصفحة بناء قسم NPA من Math Lab كصفحة دليل مستقلة: الحالة العامة، نموذج الثقة، مسار البرهان، سجل الادعاءات، المستودعات، المصادر، وصياغة واضحة بأنه ليس بديلًا.
- الحالة العامة
- مستودع بحثي
- يُعرض كبحث وتنفيذ، وليس كخدمة ضمان إنتاجية.
- إعادة تحقق عامة
- 2026-07-02 / NPA v0.2.0
- آخر وسوم git التي تم فحصها: npa v0.2.0 وnpa-std v0.1.0 وnpa-mathlib v0.1.30.
- الترخيص
- Apache-2.0
- تم التحقق من Apache-2.0 لـ npa وnpa-std وnpa-mathlib في 2026-07-02.
إعادة تحقق عامة: 2026-07-02. أحدث وسم git لمستودع NPA هو v0.2.0؛ وnpa-std هو v0.1.0؛ وnpa-mathlib هو v0.1.30. تُعرض تثبيتات README للحزم كسياق خاص بكل مستودع، ولا تُدمج في ادعاء إصدار واحد لـ NPA.
الحالة العامة
اذكر ما هو عام، وما هو دليل، ومتى أُعيد فحصه.
تجعل هذه الصفحة أساسها مرئيًا: لقطة حقيقة محلية، ومصدر مستودع عام، وتاريخ قراءة التحقق النهائية قبل الإطلاق.
إعادة تحقق عامة
2026-07-02
اكتملت قراءة التحقق من المصدر العام في 2026-07-02. وما زال إعادة بناء المصدر الأصلي يستخدم لقطة الحقيقة المحلية بتاريخ 2026-06-21.
الدليل
شهادات وتجزئات
تسجل لقطة المصدر .npcert القياسي وcertificate_hash وexport_hash وaxiom_report_hash وأحكام المدققين.
الترخيص
Apache-2.0 مؤكد
تم التحقق من Apache-2.0 لمستودعات npa وnpa-std وnpa-mathlib عبر بيانات LICENSE العامة في 2026-07-02.
الحدود
ليس NPA بديلًا عمليًا عن Lean أو Rocq. ولا تشغّل محاكاة الفحص الموزعة في المتصفح NPA نفسه. تم فحص الوسوم العامة والترخيص وظهور المستودعات في 2026-07-02 لقراءة التحقق النهائية قبل النشر.
حدود الثقة
انقل شهادة قياسية فقط عبر حدود الدليل.
لا تتعلق الحدود بمدى تطور الأداة ظاهريًا. بل تتعلق بالأثر المسموح له بأن يصبح دليلًا بعد فحص مستقل.
يبقى المحلل، والموسّع، والتكتيكات، والأتمتة، وبحث المبرهنات، والإضافات، وأنظمة الذكاء الاصطناعي، وملفات المصدر، وملفات إعادة التشغيل، وفهارس المبرهنات، وخطط النشر، وحالة CI، وصفحات الإصدارات، وبيانات السجل في جهة المرشحات غير الموثوقة.
مسار البرهان / محاكاة تفسيرية
اعرض المسار الدقيق من بايتات الشهادة إلى دليل الفحص.
لا تشغّل محاكاة المتصفح NPA نفسه ولا Rust ولا WASM ولا شهادات برهان حقيقية. إنها تعرض ترتيب الفحص غير المعتمد على المصدر الذي يجب أن تفي به الآثار الحقيقية.
مسار دليل CLI
npa package verify-certs --root . --checker reference --json
NPA / أثر التدقيق
جاهز
- 01 صيغة الشهادةبايتات .npcert القياسية / شهادة قابلة للتحليل / فحص الصيغة انتظار
- 02 تجزئة الشهادةبايتات الشهادة / certificate_hash / ملخص حتمي انتظار
- 03 حكم النواةالشهادة / قبول أو رفض / تقرير مدقق Rust انتظار
- 04 المدقق المرجعيشهادة مثبتة بتجزئة / قبول أو رفض مستقل / تقرير مدقق بلا مصدر انتظار
- 05 تقرير البديهياتحزمة مفحوصة / axiom_report_hash / جرد الافتراضات انتظار
الحكم
لم يعمل المسار التفسيري بعد.شغّل الشرح لتمييز مسار الفحص غير المعتمد على المصدر بالترتيب.
سجل الادعاءات
افصل الدليل والحقائق الحساسة للوقت وادعاءات الحدود.
لا تعتمد الصفحة على نص بحثي عام. كل عبارة عامة مرتبطة بلقطة حقيقة محلية ومصدر وإجراء نشر.
| الادعاء | الصياغة العامة | الحالة | المصدر | إجراء النشر |
|---|---|---|---|---|
| CL-001 | يعتمد NPA على الشهادة أولًا: فالحد القابل للتدقيق هو أثر .npcert القياسي ومسار الفحص المحيط به. | ادعاء عام تم التحقق منه | S01 / 2026-07-02 | راجعه عند تغيّر README. |
| CL-002 | أظهرت إعادة التحقق العامة في 2026-07-02 أن أحدث وسم git لمستودع NPA هو v0.2.0. وما زالت ملفات README للحزم المرتبطة تعرض تثبيتات خاصة بكل مستودع، لذلك تبقى صياغة الإصدار محصورة في نطاق المستودع. | إعادة تحقق عامة مؤكدة | S01 / S02 / 2026-07-02 | أبقِ صياغة الوسوم محددة حسب المستودع. |
| CL-003 | تسجل لقطة الحقيقة المحلية تثبيت سلسلة أدوات Rust 1.95.0، ولا تُستخدم هذه المعلومة كادعاء تسويقي. | تم التحقق منه، وحساس للوقت | S01 / 2026-07-02 | أعد التحقق إذا عُرض إصدار سلسلة الأدوات. |
| CL-004 | ليس NPA بديلًا عمليًا عن Lean أو Rocq. يجب أن يبقى هذا الحد واضحًا بجانب أي مقارنة. | ادعاء حدود تم التحقق منه | S01 / S03 / S05 / 2026-07-02 | احتفظ بإخلاء المسؤولية. |
| CL-005 | يمثل npa-std وnpa-mathlib مستودعين عامين منفصلين لحزم المبرهنات داخل منظمة finitefield-org. | ادعاء عام تم التحقق منه | S01 / S02 / 2026-07-02 | أعد التحقق من ظهور المستودعات إذا تأخر النشر أو تغيرت المستودعات. |
| CL-006 | تعرض مستودعات npa وnpa-std وnpa-mathlib ترخيص Apache-2.0 عبر بيانات LICENSE العامة لكل منها. | ادعاء عام تم التحقق منه | S01 / S02 / 2026-07-02 | أعد فحص LICENSE عند أي إصدار رئيسي. |
المستودعات والترخيص
أبقِ الكود ومستودعات الحزم وظهور المنظمة صريحًا.
روابط المستودعات مؤشرات إلى مصدر عام، وليست ضمانًا بأن هذه الصفحة متزامنة مع أحدث حالة على GitHub.
4 مستودعات معروضة
finitefield-org
npa
سلسلة أدوات للمساعدة في البرهان والتحقق منه بالاعتماد على الشهادة أولًا.
- الترخيص
- تم التحقق من Apache-2.0 من LICENSE في 2026-07-02.
- التحقق
- أحدث وسم git: v0.2.0. لا يوجد أحدث إصدار GitHub منشور. مرجع سلسلة الأدوات الحالي في README: NPA_GIT_TAG=v0.2.0.
تجريبيRust / OCamlالشهادة أولًا
افتح المستودع
finitefield-org
npa-std
مستودع حزمة مبرهنات قياسية لمصادر براهين NPA.
- الترخيص
- تم التحقق من Apache-2.0 من LICENSE في 2026-07-02.
- التحقق
- أحدث وسم git وأحدث إصدار GitHub: v0.1.0. إصدار بيانات الحزمة في README: 0.1.0؛ وتثبيت سلسلة أدوات الحزمة: NPA_GIT_TAG=v0.1.1.
تجريبيحزمة مبرهناتمصدر برهان
افتح المستودع
finitefield-org
npa-mathlib
مستودع بحثي لمكتبة رياضيات شكلية.
- الترخيص
- تم التحقق من Apache-2.0 من LICENSE في 2026-07-02.
- التحقق
- أحدث وسم git: v0.1.30. أحدث إصدار GitHub: v0.1.9. إصدار بيانات الحزمة في README: 0.2.1؛ وتثبيت سلسلة أدوات الحزمة: NPA_GIT_TAG=v0.1.1.
بحثرياضيات شكليةمكتبة
افتح المستودع
finitefield-org
منظمة Finite Field على GitHub
لقطة عامة لعائلة مستودعات Lab.
- الترخيص
- تنطبق تراخيص كل مستودع على حدة
- التحقق
- كانت npa وnpa-std وnpa-mathlib عامة عند قراءة تحقق GitHub API في 2026-07-02.
فهرس عاملقطة ظهورمصدر
افتح المنظمة
لا يوجد مستودع يطابق البحث الحالي.
مستودعات GitHub هي مصدر حالة الكود العام. تم فحص الترخيص والوسوم الحالية والظهور العام وصياغة الإصدارات في 2026-07-02 بوصف ذلك قراءة التحقق النهائية لـ M10-T14.
حارس منظومة البرهان
وضّح الأدوار قبل مقارنة أدوات البرهان.
هذا جدول أدوار وليس ترتيبًا للأفضلية. تبقى Lean وRocq منظومتين مرجعيتين لمساعدات البرهان، بينما يُعرض NPA كعمل بحثي وتنفيذي يتمحور حول الشهادة.
| البند | Lean | Rocq | NPA |
|---|---|---|---|
| الموقع | لغة برمجة ومساعد برهان مفتوح المصدر. | مبرهن نظريات تفاعلي له تاريخ بحثي طويل. | مستودع بحث وتنفيذ للفحص المرتكز على الشهادة. |
| الاستخدام المعتاد | الرياضيات، والتحقق من البرمجيات، والبرمجة. | الرياضيات، والمواصفات، والتحقق من البرامج، والاستخراج. | بحث في شهادات البرهان، والفحص المستقل، وقاعدة الثقة الصغيرة. |
| حد الدليل | تحدد نواته الموثوقة ومنظومته الخاصة حدود الفحص. | تحدد نواته الخاصة والتطويرات المفحوصة حدود الفحص. | ينتقل أثر .npcert القياسي من التوليد إلى الفحص. |
| كيف تتعامل هذه الصفحة معه | مرجع للتعلم والمقارنة والتشغيل البيني. | مرجع للتعلم والمقارنة وطرائق الصياغة الشكلية. | مشروع بحثي من Finite Field، وليس وعدًا بمنتج. |
| الحدود | ما زالت المعرفة المتخصصة مطلوبة. | ما زالت المعرفة المتخصصة مطلوبة. | ليس NPA بديلًا عمليًا عن Lean أو Rocq في الوقت الحالي. |
المصادر
انشر خريطة المصادر بجانب التفسير.
تُعرض المصادر حتى يعرف القارئ أي الادعاءات تأتي من مستودعات عامة أو مواقع رسمية لأدوات البرهان أو سياق الشركة.
S01
finitefield-org/npa
مصدر أساسي لغرض NPA ونموذج الثقة وصياغة وسم المستودع الحالي v0.2.0 والأوامر وبنية المستودع والترخيص.
افتح المصدر S02منظمة Finite Field على GitHub
مصدر أساسي لظهور المستودعات العامة وأحدث وسوم git وصفحات الإصدارات ولقطة عائلة مستودعات Lab التي فُحصت في 2026-07-02.
افتح المصدر S03الموقع الرسمي لـ Lean
مصدر أساسي للتموضع العام لـ Lean، فُحص في 2026-07-02.
افتح المصدر S04مرجع لغة Lean
مصدر أساسي لسياق نظرية الأنواع التابعة ومرجع النواة، فُحص في 2026-07-02.
افتح المصدر S05الموقع الرسمي لـ Rocq Prover
مصدر أساسي للتموضع العام لـ Rocq، فُحص في 2026-07-02.
افتح المصدر S06موقع شركة FINITE FIELD
مصدر الشركة لعلامة Finite Field وسياق الأعمال.
افتح المصدرأسئلة شائعة
حالة NPA وحدود التحقق.
تؤكد الإجابات حد الثقة قبل أن يخلط القارئ بين صفحة بحثية وخدمة مساعد برهان منشورة.
اقرأ عن الشركة01 هل تمثل هذه الصفحة ضمانًا لمنتج؟
لا. يُعرض NPA هنا كمستودع بحث وتنفيذ.
02 هل يمكن أن يحل NPA محل Lean أو Rocq؟
لا. ليس NPA بديلًا عمليًا عن Lean أو Rocq.
03 هل تشغّل الصفحة تحقق NPA الحقيقي؟
لا. لا تشغّل محاكاة المتصفح NPA نفسه ولا Rust ولا WASM ولا شهادات برهان حقيقية.
04 ما الذي يُعد دليلًا هنا؟
يتكون دليل جهة الفحص من أثر الشهادة، والتجزئات الحتمية، ونتيجة نواة/مدقق Rust، ونتيجة المدقق المرجعي غير المعتمد على المصدر، وتقرير البديهيات.
05 ما الحقائق التي تحتاج إلى إعادة تحقق؟
أعيد التحقق من الإصدار العام الحالي وظهور المستودعات وتثبيتات سلسلة الأدوات ونص الترخيص وصياغة المصدر في 2026-07-02.
من انضباط البرهان إلى العمليات
استخدم الانضباط نفسه في الأدلة عندما يجب الوثوق بقرار أعمال.
في أنظمة الأعمال، ليست الفائدة العملية أن نضيف البرهنة النظرية في كل مكان. الفائدة هي تحديد ما يجب توليده وفحصه وتسجيله وتصحيحه واعتماده من البشر.