تيرنس تاو يكتب للرياضيين عن موثوقية Lean ودور الذكاء الاصطناعي

في 9 أكتوبر 2026 نشر تيرنس تاو في مدونته منشورًا بعنوان «What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI». ويتضح من العنوان أن المنشور موجّه إلى الرياضيين المحترفين الذين يتابعون التحقق الشكلي وأنظمة الذكاء الاصطناعي التي تكتب البراهين. حصدت التدوينة على Hacker News مجموع 53 نقطة و7 تعليقات. وصلنا رابط المنشور فقط من دون نصه، ولذلك لا نعرض حجج الكاتب. نستعرض أدناه السياق الذي يظهر فيه منشور كهذا وسبب أهميته.

لماذا أصبح سؤال الموثوقية عمليًا

بدأ Lean مشروعًا أطلقه ليوناردو دي مورا في Microsoft Research عام 2013. وهو اليوم أداة عمل تُستخدم في مشاريع جماعية كبيرة. شارك تاو نفسه في أواخر عام 2023 في إضفاء الصيغة الشكلية على حدسية PFR، واستغرقت العملية نحو ثلاثة أسابيع. وفي عام 2024 نسّق مشروع Equational Theories Project، الذي تطلّب تحديد 22 028 942 استلزامًا بين 4694 متطابقة على الماغمات. ومن دون الأتمتة والتحقق الشكلي، لما استطاع البشر ولا المحكّمون التعامل مع حجم كهذا.

وفي الوقت نفسه بدأت نماذج اللغة العمل داخل Lean. ففي يوليو 2024 حلّ نظام AlphaProof من Google DeepMind أربع مسائل من أصل ست في IMO، وحصل على 28 نقطة من 42. وقد أنتج البراهين بصيغة Lean. ومنذ ذلك الحين لم يعد السؤال «هل يمكن الوثوق بما يخرج من سلسلة كهذه» شأنًا من فلسفة الرياضيات، بل صار جزءًا من العمل اليومي.

أين يقع حد الثقة

لدى Lean نواة صغيرة تتحقق من كل حدّ (term) في البرهان. أما التكتيكات والأتمتة والشيفرة التي يولّدها النموذج فتقع خارج النواة. وإذا أخطأت، فإن النواة سترفض النتيجة ببساطة. وهذا ما يجعل الجمع بين Lean والذكاء الاصطناعي جذابًا: فالهلوسة في البرهان تُكتشف آليًا.

تبقى مواضع تحتاج فيها الثقة إلى تقييم مستقل:

• صياغة النظرية. تؤكد النواة أن العبارة المكتوبة قد أُثبتت. أما مطابقتها للمقصود فيحكم فيها الإنسان.
• التعريفات. يجعل التعريف غير الدقيق في المكتبة أو في الملف النظرية المُثبتة بلا مضمون.
• البديهيات. يعتمد Lean على `propext` و`Classical.choice` و`Quot.sound`. ويعرض الأمر `#print axioms` البديهيات المستخدمة.
• `sorry`. هي عنصر نائب يحل محل البرهان. يُترجم الملف الذي يحتويها بنجاح، لكن النظرية لا تكون مُثبتة.
• `native_decide`. تضيف هذه التكتيكية المُصرِّف إلى قاعدة الثقة، ويظهر `Lean.ofReduceBool` في قائمة البديهيات.
• تنفيذ النواة. توجد برامج تحقق مستقلة، مثل lean4checker وعمليات إعادة تحقق من جهات خارجية، تقلل خطر وقوع خطأ في النواة نفسها.

ما الذي يغيّره الذكاء الاصطناعي

قبل ظهور النماذج كان القيد الرئيسي هو جهد من يضفي الصيغة الشكلية. يخفف النموذج جزءًا من هذا العبء، لأنه يقدّم مئات المرشحين للبرهان. ويبقى التحقق بواسطة النواة زهيد الكلفة. لكن المهمة الثانية تتقدم إلى الواجهة، وهي التأكد من أن العبارة الشكلية تقول فعلًا ما قصده المؤلف. هذا العمل لا تؤديه النواة، وقد يجد النموذج الذي يكيّف البرهان مع الصياغة ثغرات في الصياغة نفسها. ومن الأمثلة النمطية عبارة تتحقق بصورة تافهة بسبب مجموعة فارغة أو قسمة على الصفر معرّفة تعريفًا غير موفق.

ويترتب على ذلك استنتاج عملي: ينتقل التدقيق من خطوات البرهان إلى شروط المسألة. وهذا بالنسبة إلى الرياضيين تغيّر في المهارة المطلوبة أكثر منه فقدانًا للسيطرة.

كيف نتعامل مع هذا

إذا كنت تنوي استخدام Lean أو مساعد ذكاء اصطناعي في عمل بحثي، فمن المفيد اتباع تسلسل قصير من الخطوات:

• اكتب صياغات النظريات أو أعد قراءتها بنفسك، حتى لو ولّد النموذج البرهان.
• قبل النشر شغّل `#print axioms` وابحث عن `sorry`.
• تحقق من أن التعريفات المستخدمة من Mathlib تطابق فهمك. وفي الحالات غير المعتادة اكتب أمثلة مضادة ولِمّات للتحقق.
• في النتائج الحرجة مرّر الملف عبر أداة تحقق مستقلة.
• اقرأ منشور تاو الأصلي. قدّمنا هنا السياق، أما حججه وتوصياته فالأفضل أخذها من المصدر الأول.