Lean مبرهن النظريات أمام أسئلة الموثوقية مع تطور الأتمتة الرسمية لـ AI

الصياغة الرسمية والأتمتة الرسمية

أصبح Lean هو مبرهن النظريات الأكثر شعبية بين الرياضيين، وفقاً لمنشور الضيف للرياضي توماس هيلز. أنشأه ليو دي مورا عام 2013 أثناء عمله في Microsoft؛ ثم نشرت Microsoft البرنامج لاحقاً مفتوح المصدر. يعتمد Lean على نظرية الأنواع، وتحديداً على حساب الإنشاءات الاستقرائية. مكتبة mathlib المجتمعية التي بدأت عام 2017، تضم الآن نحو 300 000 نظرية، وأكثر من 100 000 تعريف، و2,5 مليون سطر من التعليمات البرمجية، وأكثر من 700 مساهم. يمكن استخدام أي نظرية في mathlib في براهين لاحقة بدلاً من إعادة إثباتها.

أصبحت الأتمتة الرسمية، عندما يقرأ AI العمل ويصدر إثباتاً رسمياً، واقعاً عملياً في 2026. ومن بين المراحل المهمة: شبه الأتمتة الرسمية لنظرية الأعداد البسيطة بواسطة Math Inc. في سبتمبر 2025، وصياغة جزء كبير من كتاب طوبولوجيا Munkres رسمياً، ومسألة تغليف الكرات في 24 بُعداً، وأتمتة Anthropic لنظرية فيرما الأخيرة في 4 سبتمبر، والتي ولّدت 13 مليون سطر من Lean في 11 يوماً، وصياغة OpenAI لانفجارات Navier-Stokes، التي أُعلن عنها في 8 سبتمبر.

التصميم ونموذج الموثوقية

يجمع Lean بين لغة برمجة ذات غرض عام ولغة رياضية للتعريفات وصيغ النظريات وسكربتات الإثبات. تقوم سكربتات الإثبات بتحليل ومعالجة وفحص نواة Lean، وهي بضعة آلاف من أسطر كود C++. يؤكد المنشور أن إثباتات Lean لا يجب أن تُعتمد أبداً قبل فحصها بواسطة النواة، وأنه يلزم تدقيق بشري منفصل لتأكيد صياغة النظرية بأمان، حتى تتأكد أن النظرية المؤكدة هي بالفعل النظرية التي يقصدها الرياضيون.

صيف ثغرات الموثوقية

ثغرة الموثوقية هي ثغرة في النواة تسمح بإثبات «False»، وبالتالي إثبات أي عبارة. ظهرت عدة ثغرات من هذا النوع في Lean في يوليو وأغسطس 2026، والتي تُسمى الآن صيف ثغرات الموثوقية. تسببت إحداها في دحض غير قانوني لفرضية كولاتز، وأخرى في إثبات غير قانوني مختصر لفرضية كبلر. تم إصلاح جميعها بسرعة، وتم فحص mathlib بالنواة المصححة.

الاقتراحات والمشكلات المفتوحة

تتم مناقشة ثلاثة ردود. أولاً، كتابة نوى Lean إضافية وفحص الإثباتات بشكل متقاطع؛ يوجد نحو 25 نواة، وقد أكد أكثر من عشرة مدققين للإثبات صياغة Navier-Stokes. ثانياً، فحص النواة رسمياً كما فعل يواخيم برايتنر باستخدام Con-Leche، مع نواة Lean مؤكدة، تم توليد إثبات اتساقها بواسطة Claude وفحصت mathlib. ثالثاً، تعميق الفهم النظري لنظرية الأنواع في Lean، حيث لا يزال التصنيف الفريد، وحقن Pi، وخاصية Church-Rosser المعدلة، وإثبات الاتساق العلني العلائقي الكامل مفتوحة. ينتهي المنشور باقتباس من «Reflections on Trusting Trust» لكين تومسون ويحذر من أن الثقة العمياء في أنظمة مثل Lean لم تعد ممكنة.

المصادر: terrytao.wordpress.com