Lean 4 Verify — طبقة تحقّق برهاني رسمي (double-check رياضي)

الغرض: بعد حلّ أي مسألة رياضية/منطقية (opus5-clean-executor أو الشات)، نتحقّق من صحة النتيجة بإثبات صوري رسمي في Lean 4 — لا احتمالي. طبقة double-check موازية.

الحالة: Lean 4.34.1 + Lake 5.0 مثبّت (/data/.elan/bin/). مُثبَت حيّاً 2026-09-28 (selftest 3/3 + كشف خطأ متعمّد).

الاستخدام


python3 skills/lean-verify/lean_verify.py verify-eq "<expr>" "<value>"   # تحقّق حسابي
python3 skills/lean-verify/lean_verify.py check "<lean theorem code>"     # نظرية جاهزة
python3 skills/lean-verify/lean_verify.py selftest

متى يُستدعى (اختياري لا تلقائي)

بعد حلّ مسألة حسابية/منطقية حرجة → double-check برهاني قبل التسليم.
المسائل الرمزية/المنطقية (nat/int/logic) — النطاق المؤكّد بلا mathlib.

النطاق والقيود (صادقة)

✅ يعمل: الحساب المباشر (rfl)، المنطق الأساسي، Nat/Int، decide.
❌ بلا mathlib (غير مبنيّ): لا تكامل/جبر خطي/دوال متقدّمة. mathlib بناؤه ثقيل — يُبنى عند حاجة فعلية.
fail-safe: أي تعذّر → unverified لا ينهار (never-stop).
الحالات الثلاث: proven (verified=true) · unverified (تعذّر) · disproven/FALSE (خطأ مكشوف).

التكامل

double-check موازٍ لـ opus5-clean-executor (المسار الرياضي النظيف).
الأداة: skills/lean-verify/lean_verify.py. Lean: /data/.elan/bin/lean.

🧭 طبقة Lean Atlas — تحقّق دلالي (semantic hallucination) — جديد 2026-10-06

الغرض: براهين AI قد تمرّ type-checker لكن لا تمثّل المحتوى الرياضي المقصود (هلوسة دلالية). Lean Atlas (github.com/NyxFoundation/lean-atlas) يحلّها عبر رسم اعتماديات تفاعلي + Lean Compass (يستخرج العقد التي تؤثّر على نظرية هدف → تقليل المراجعة البشرية 27-99%). الحالة: بُني ويعمل حيّاً على Lean 4.34.1 (رغم أنه مكتوب لـ v4.28.0) — مُثبَت 2026-10-06: atlas graph-data = 313 عقدة/611 حافة + Lean Compass Reduction Analysis. الاستخدام (الجسر):


bash skills/lean-verify/lean_atlas.sh graph [project_dir]    # رسم اعتماديات graph.json
bash skills/lean-verify/lean_atlas.sh compass [project_dir]  # Lean Compass reduction
bash skills/lean-verify/lean_atlas.sh selftest              # تحقّق التشغيل