باختصار
مساعد البراهين (Proof Assistant) برنامج تكتب فيه البرهان الرياضي بلغة صارمة، فيتحقّق من كل خطوة فيه، ولا يقبل أيّ قفزة لم تُبرَّر.
بالتفصيل
أشهر الأمثلة اليوم Lean، وهو بحسب موقعه لغة برمجة وظيفية ومثبت مبرهنات بُني لصياغة الرياضيات صوريًا وللتحقّق الصوري. ومعه مكتبة رياضية مشتركة اسمها Mathlib، يبني عليها الرياضيون بعضهم فوق عمل بعض.
ما الذي يغيّره ذلك؟ يقول Terence Tao، في شهادة على موقع Lean، إن اللغة تتيح تعاونًا واسعًا لأنها تسمح بتقسيم البراهين المعقّدة إلى أجزاء أصغر يمكن التحقّق من كل منها. ويقول Pushmeet Kohli من Google DeepMind إن فريقه استخدم Lean لبناء AlphaProof، نظامه للاستدلال الرياضي الصوري.
ومع النماذج اللغوية صار لمساعد البراهين دور جديد: حكَم محايد. النموذج قد يهلوس، لكن Lean لا يجامل. إذا قبل البرهان، فالمنطق سليم بشرط أن تكون صياغة المسألة نفسها صحيحة، ولا تحتاج حينها أن تثق بالنموذج. ولهذا يذكر موقع Lean أن OpenAI وAnthropic نشرتا نتائج رياضية مصحوبة ببراهين صورية مكتوبة بلغة Lean.
وللمبتدئين، يقترح موقع Lean «لعبة الأعداد الطبيعية» (Natural Number Game) مدخلًا ممتعًا.
مثال عملي
تذكّر مدرّس الرياضيات الصارم الذي كان يشطب «من الواضح أن» بالقلم الأحمر، ويكتب في الهامش: «وضّح!».
مساعد البراهين هو هذا المدرّس، لكنه لا يتعب ولا يملّ، ويقرأ الصفحة الألف بالدقّة نفسها التي قرأ بها الصفحة الأولى.
مصطلحات مرتبطة
- Formal Verification — التحقّق الصوري.
- Automated Theorem Proving — الإثبات الآلي للمبرهنات.
- Reasoning Model — نموذج الاستدلال.
- Hallucination — الهلوسة.
المصادر: Lean Learn، Lean
