كيف يعمل Lean، البرنامج الذي لا يثق بمن يبرهن

في 4 سبتمبر، نشرت Anthropic أول برهان كامل لمبرهنة فيرما الأخيرة يتحقق منه حاسوب. تقول المبرهنة إنه لا توجد أعداد صحيحة موجبة a وb وc بحيث يكون aⁿ + bⁿ = cⁿ عندما يكون n أكبر من 2. دوّنها فيرما نحو عام 1637 على هامش كتاب، ونشر أندرو وايلز (Andrew Wiles) أول برهان صحيح عليها عام 1995، بعد أكثر من 350 عامًا من المحاولات الفاشلة.

لم تعثر Anthropic على برهان جديد. بل أعادت كتابة برهان وايلز، في الصيغة التي عرضها دارمون (Darmon) ودايموند (Diamond) وتايلور (Taylor)، بلغة تُسمّى Lean. أنجز ذلك عشرات من وكلاء Claude خلال 11 يومًا، مع توجيهات بشرية متفرقة. وتشغل النتيجة 13 مليون سطر: أكثر من خمسة أضعاف حجم Mathlib، المكتبة الكبيرة من الرياضيات المُتحقَّق منها التي يتولاها المجتمع.

لن يقرأ أحد 13 مليون سطر. ومع ذلك، راجعه كيفن بازارد (Kevin Buzzard)، عالم الرياضيات في إمبريال كوليدج لندن الذي يقود منذ 2024 المشروع المجتمعي لصياغة البرهان نفسه صياغة رسمية، وخلص إلى أنه يبرهن على المبرهنة دون أي افتراضات سوى بديهيات الرياضيات.

بعد خمسة أيام، نشرت شركة الأمن Trail of Bits «برهانًا» آخر لمبرهنة فيرما. كان يتسع في شاشة واحدة، وكان Lean يَسِمه هو الآخر بأنه صحيح.

الأمران صحيحان، وفهم السبب هو فهم طريقة عمل Lean. في المقال عن براهين OpenAI الـ722 فصلنا طبقات ما يعنيه أن تكون نتيجة ما «مُتحقَّقًا منها». وهنا ننظر داخل الطبقة الأولى: ما الذي يفعله البرنامج بالضبط، وأي جزء منه يجب أن نصدّقه، وماذا حدث هذا العام حين أخفق ذلك الجزء.

برهان يُصرَّف

Lean لغة برمجة ومساعد براهين في آن واحد: برنامج يُكتب فيه البرهان بتفصيل يكفي لأن يراجع الحاسوب كل خطوة فيه. بدأه ليوناردو دي مورا (Leonardo de Moura) في Microsoft Research عام 2013، ومنذ 2023 تطوّره Lean FRO، وهي منظمة غير ربحية أُنشئت لهذا الغرض.

أسرع طريقة لفهم ما يفعله هي أن نعطيه عبارتين بسيطتين، إحداهما صحيحة والأخرى خاطئة:

example : 2 + 2 = 4 := rfl

example : 2 + 2 = 5 := rfl

Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  2 + 2 = 5

تقول رسالة الخطأ type mismatch، أي عدم تطابق في الأنواع: وهو الخطأ نفسه الذي يعطيه المصرِّف حين يُمرَّر نص في موضع يُنتظر فيه عدد. وليس هذا مجرد تشابه في المفردات. ففي Lean، العبارة نوع، والبرهان قيمة من ذلك النوع. والتحقق من برهان يعني التحقق من أن القيمة من النوع الصحيح، تمامًا كما يتحقق المصرِّف من أن دالة تُعيد ما تقول إنها تُعيده.

يُعرف هذا التكافؤ بين البراهين والبرامج باسم «القضايا بوصفها أنواعًا» أو تناظر كاري–هوارد (Curry-Howard). اكتشفه المناطقة تدريجيًا بين ثلاثينيات القرن الماضي وستينياته، وهو أساس Lean ومساعدات براهين أخرى مثل Rocq وAgda. ولمن يبرمج، يسهل تخيّل النتيجة: أن يكون البرهان صحيحًا يعني أنه يُصرَّف.

كتابة برهان حوارٌ مع Lean

لا يكاد أحد يكتب تلك القيم يدويًا. المعتاد استخدام التكتيكات: أوامر مثل «طبّق الاستقراء» أو «أعد الكتابة باستخدام هذه المساواة»، تحوّل تدريجيًا ما بقي البرهان عليه. وفي كل خطوة، يعرض Lean حالة البرهان: ما المعطيات المتاحة وما الهدف المتبقي، مُعلَّمًا بالرمز ⊢.

مثال كامل: البرهان على أن إضافة صفر من اليسار تُبقي العدد الطبيعي كما هو. يبدو الأمر بديهيًا، لكنه ليس كذلك في Lean. فالجمع معرَّف بالمرور على العدد الثاني، ولذلك ينتج n + 0 = n مباشرةً من التعريف، بينما يجب البرهان على 0 + n = n.

theorem cero_mas (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [← Nat.add_assoc, ih]

n : Nat
⊢ 0 + n = n

k : Nat
ih : 0 + k = k
⊢ 0 + (k + 1) = k + 1

⊢ 0 + k + 1 = k + 1

المثير للاهتمام هو ما يحدث حين تفشل خطوة. إذا تجاوزنا إعادة التجميع وكتبنا مباشرةً rw [ih]، فإن Lean لا يكتفي بالرفض:

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  0 + k
in the target expression
  0 + (k + 1) = k + 1

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

تحت التكتيكات يوجد برنامج

التكتيكات ليست البرهان: إنها برامج تبنيه. إذا طلبنا من Lean أن يعرض ما حفظه باسم cero_mas، يظهر هذا:

theorem cero_mas : ∀ (n : Nat), 0 + n = n :=
fun n =>
  Nat.recAux (Eq.refl (0 + 0))
    (fun k ih =>
      Eq.mpr (id (congrArg (fun _a => _a = k + 1) (Eq.symm (Nat.add_assoc 0 k 1))))
        (Eq.mpr (id (congrArg (fun _a => _a + 1 = k + 1) ih)) (Eq.refl (k + 1))))
    n

إنها دالة تبني البرهان لكل n بالعودية، عبر سلسلة من المساواة. لا أحد يكتبها هكذا؛ بل تولّدها التكتيكات. وهذا الكائن، الذي يُسمّى حدّ البرهان، هو ما يُتحقَّق منه.

هذا الفصل هو أهم قرار تصميمي في Lean. يمكن أن تكون التكتيكات متطورة بالقدر الذي نريد. فهناك تكتيكات تحل وحدها مسائل حسابية، مثل omega، وأخرى تبحث عن تركيبات من حقائق معروفة، مثل grind، ويستطيع أي شخص أن يكتب تكتيكاته الخاصة. ولا يحتاج أيٌّ منها إلى أن يكون صحيحًا. فكل ما تنتجه ينتهي محوَّلًا إلى حدٍّ مثل الذي في الأعلى، وهذا الحدّ يراجعه مكوّن صغير يُسمّى النواة (kernel)، لا يعرف إلا القواعد الأساسية لمنطق Lean. وإذا كان في تكتيك ما خطأ فبنى شيئًا غير صالح، رفضته النواة. ويعدّ الدليل الرسمي للتحقق من صحة برهان أخطاء التكتيكات ضمن ما يغطيه التصريف وحده.

تُعرف فكرة أن تنتج آلية كبيرة النتائج ويراجعها مدقق صغير بمعيار دي براون (De Bruijn)، نسبةً إلى عالم الرياضيات الهولندي الذي طبّقها في نظامه Automath في أواخر الستينيات.

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

ثلاث بديهيات وsorry

قبول النواة لشيء ما لا يكفي لمعرفة ما الذي بُرهن عليه. فـLean يسمح بالعمل مع فجوات ومع افتراضات، ومن السهل أن يغفل المرء عن كليهما.

الفجوة اسمها sorry: كلمة تُكتب في موضع برهان لم يُنجَز بعد. يقبلها Lean حتى يمكن التقدم جزءًا جزءًا، لكنه ينبّه إليها ويسجّلها. أما الافتراضات فهي البديهيات، أي عبارات تُقبل دون برهان. يأتي Lean بثلاث منها افتراضيًا، تعدّها الممارسة الرياضية المعتادة مقبولة رغم أسمائها غير المألوفة:

• propext: عبارتان تستلزم كل منهما الأخرى هما العبارة نفسها.
• Quot.sound: يمكن معاملة كل الكائنات التي نعدّها متكافئة على أنها كائن واحد. وهي العملية التي تُبنى بها، مثلًا، الكسور انطلاقًا من أزواج من الأعداد الصحيحة، حيث 1/2 و2/4 هما العدد نفسه.
• Classical.choice: من مجموعة غير خالية يمكن اختيار عنصر، حتى لو لم نعرف أيّها. إنها بديهية الاختيار.

لكن يستطيع أي شخص أن يضيف المزيد، بما في ذلك بديهيات خاطئة. ولذلك فإن أهم أمر لمراجعة برهان كتبه غيرنا ليس تصريفه، بل سؤال Lean عمّا يعتمد عليه، باستخدام #print axioms. مع أمثلتنا:

theorem trampa : 2 + 2 = 5 := by sorry

theorem cero_mas' (n : Nat) : 0 + n = n := by
  omega

'cero_mas' does not depend on any axioms
'cero_mas'' depends on axioms: [propext, Quot.sound]
'trampa' depends on axioms: [sorryAx]

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

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem

«البرهان» الذي اتسع له الهامش

الآن تتضح حيلة Trail of Bits. فقد استخدم برهانهم native_decide، وهو تكتيك لا يترك الحساب للنواة طلبًا للسرعة، بل ينفّذه بوصفه كودًا مصرَّفًا. وهو مفيد للحسابات الكبيرة، لكن له ثمنًا: فإلى جانب النواة، يجب الوثوق بالمصرِّف. ويسجّل Lean ذلك بإضافة بديهية إلى القائمة.

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

كان المحرر يعرض علامات «صحيح» الزرقاء. لكن #print axioms كان يضيف إلى البديهيات المعيارية الثلاث واحدة أخرى: flt._native.native_decide.ax_1_1. وأوضحت Trail of Bits نفسها أن الخلل لم يكن في النواة. أصلح فريق Lean الجزء الأخطر في نحو ثلاث ساعات، والباقي بعد خمسة أيام. وكان الخطأ يمسّ جميع الإصدارات المستقرة حتى 4.33.1، وهو تحديدًا الإصدار الذي يستخدمه مستودع فيرما الخاص بـAnthropic. لكن ذلك المشروع لم يتأثر: فهو يحظر native_decide ويشترط البديهيات الثلاث بالضبط.

الدرس عملي. الحكم ليس العلامة الزرقاء في المحرر، بل قائمة البديهيات. والدليل الرسمي يقول ذلك صراحةً: تظهر العلامات الزرقاء حتى لو استخدمت إحدى القطع التي تستند إليها المبرهنة sorry، والبديهية التي يحتوي اسمها على _native تدل على أن جزءًا من الحساب أجراه كود مصرَّف.

وماذا لو كانت النواة هي التي تخطئ؟

النواة صغيرة، لكنها ليست معصومة، وقد ثبت ذلك في يوليو.

في 25 يوليو، نشر رامانا كومار (Ramana Kumar) دحضًا لحدسية كولاتز (Collatz) توصّل إليه بمساعدة الذكاء الاصطناعي. تقول الحدسية إنك إذا أخذت أي عدد صحيح موجب، وقسمته على اثنين إذا كان زوجيًا، أو ضربته في ثلاثة وأضفت إليه واحدًا إذا كان فرديًا، فستصل عاجلًا أو آجلًا إلى 1. لم يكن في الدحض أي sorry. ولم يكن صحيحًا أيضًا: فقد استغل خطأ في النواة عند التعامل مع الأنواع الاستقرائية المتداخلة، وهي أنواع معرَّفة بدلالة نفسها داخل أنواع أخرى، مثل شجرة فروعها قائمة من الأشجار.

في 28 يوليو، اختزله كيران غوبيناثان (Kiran Gopinathan) إلى برهان على القضية «الكاذبة» وأبلغ عنه. وبعد ساعة كان هناك إصلاح، نُشر في Lean 4.32.2. وقد صُرِّف برهان فيرما بالإصدار 4.33.1، الذي يتضمن هذا الإصلاح. ووفقًا للتحليل اللاحق الذي كتبه ليوناردو دي مورا، لم يكن الوصول إلى الخلل ممكنًا إلا عبر البرمجة الوصفية (metaprogramming)، أي ببرامج ترسل التصريحات مباشرةً إلى النواة دون المرور بالفحوص المعتادة.

الجزء الأكثر إفادة هو التحقق الثاني. فلأن النواة قد تخطئ، توجد نوى مستقلة: برامج كُتبت من الصفر تعيد مراجعة الحدود نفسها. وأبرزها nanoda، الذي كتبه كريس بيلي (Chris Bailey) بلغة Rust. وكان دحض كومار قد اجتاز أيضًا إصدارًا من nanoda يسبقه بأسبوع، لأنه استغل في الوقت نفسه خطأ آخر في nanoda، مختلفًا وقد أُصلح من قبل. لزم وجود خطأين لا علاقة بينهما في تطبيقين في آن واحد. واستنتاج دي مورا أن التحقق المستقل لا يزال يعمل، بشرط استخدام إصدارات محدَّثة من الاثنين. وبعد ذلك، عثر باحث في OpenAI، بمساعدة ذكاء اصطناعي متخصص في الأمن، على أخطاء أخرى في النواة، لا يمكن الوصول إليها كلها إلا بالبرمجة الوصفية. واكتشفها المدقق nanoda جميعًا.

كانت Lean FRO تختبر المدققات المستقلة علنًا في Lean Kernel Arena، وبعد يوليو أضافت إليها اختبارات هذه الأخطاء والتزمت بالاستثمار في مزيد من التطبيقات. وأبرز المدققات con-leche، الذي نُشر في سبتمبر: مدقق خارجي يرافقه برهان، مكتوب في Lean، على أنه لا يقبل أبدًا برهانًا على القضية «الكاذبة». ويذكر ملف README الخاص به أن Claude هو من نفّذه وبرهن عليه، تحت إشراف يواكيم برايتنر (Joachim Breitner) من Lean FRO، الذي يصف الكود بأنه كومة فوضوية تعمل ومُبرهَن عليها. ولا يزيل ذلك الدائرية كلها، لأن هذا البرهان تراجعه بدورها نواة Lean، لكن أي خطأ سيتعين عليه أن يتسلل عبر قطع تعمل بطرق مختلفة.

يرتّب دليل Lean الرسمي كل هذه الفحوص من الأقل إلى الأكثر صرامة. كل مستوى يضيف حماية، لكنه يترك أيضًا شيئًا خارجه:

المصدر: «Validating a Lean Proof»، الدليل المرجعي لـLean. ملخص من إعداد Codin. ويخصص الدليل المستوى الأخير للحالات عالية المخاطر، مثل المسابقات ذات الجوائز أو أنظمة الذكاء الاصطناعي التي لا يمكن افتراض حسن نيتها.

مرّ برهان فيرما الخاص بـAnthropic بالمستوى الأخير: النواة الرسمية، وإصدار من nanoda راجع 1,052,234 تصريحًا دون أخطاء، وComparator، الأداة التي تتحقق في بيئة معزولة من أن المنطوق المُبرهَن مطابق للمنطوق المرجعي. ليس هذا يقينًا مطلقًا. إنه شيء آخر: الثقة في شيء صغير، وعلني، ومُتحقَّق منه بعدة طرق.

ما لا يراجعه أي برنامج

تضمن النواة أن الحدّ يبرهن على المنطوق المكتوب. ولا تضمن أن هذا المنطوق يقول ما نظنه. ويضرب دليل المجتمع أمثلة: يمكن إعادة تعريف ما هي الأعداد الطبيعية، أو تسمية أي عبارة TheRiemannHypothesis، والبرهنة على شيء يشبه مبرهنة كبرى دون أن يكونها.

منطوق فيرما مكتوب بالأعداد الطبيعية والعمليات التي يأتي بها Lean. وحدها عملية الرفع إلى قوة تأتي من Mathlib، ويتحقق Comparator من أنها تطابق المنطوق الذي كان موجودًا بالفعل في Mathlib، والذي راجعه القائمون عليها. ولذلك يسهل الوثوق به. أما ما لا تستطيع أي أداة التحقق منه، كما ينبّه المستودع نفسه، فهو أن كل واحدة من المبرهنات الوسيطة البالغ عددها 29,511 تعني ما يوحي به اسمها. ولا يهم ذلك بالنسبة إلى النتيجة النهائية، لأن النواة تراجع كل ما تحتها. لكنه يهم إذا أراد شخص أن يتعلم شيئًا من ذلك البرهان.

هنا تكمن الوظيفة الأقل ظهورًا لـMathlib. ففي 8 أكتوبر 2026، كانت تضم 290,229 مبرهنة و137,964 تعريفًا من 772 شخصًا. وقيمتها ليست في الكمية وحدها: إنها تعريفات مشتركة ومُراجَعة، يمكن أن يُقرأ في ضوئها منطوق جديد دون الارتياب في كل كلمة. وحين تحتاج نتيجة ما إلى تعريفات لا تتضمنها Mathlib، يجب أن يراجعها شخص من أهل الاختصاص، كما شرحنا مع حالات OpenAI التي استندت إلى تعريفات خاصة.

لماذا يناسب الذكاء الاصطناعي إلى هذا الحد

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

AlphaProof من Google DeepMind هو المثال الأكثر توثيقًا. فوفقًا لمقاله في Nature، المنشور في نوفمبر 2025، تعلّم البحث عن براهين في Lean بالتعلّم المعزَّز، بطريقة مستوحاة من AlphaZero وبملايين المسائل المترجمة آليًا إلى Lean. وحقق، مع AlphaGeometry 2، في الأولمبياد الدولي للرياضيات 2024 نتيجة تعادل ميدالية فضية. وتروي Anthropic شيئًا مشابهًا في اتجاه آخر: يستخدم Claude براهين جزئية في Lean ليتحقق من فرضياته أثناء العمل، كما قد يستخدم محاكاة عددية ليرى هل يسير في الاتجاه الصحيح.

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

والتحقق ليس مجانيًا أيضًا. فقد كلّف برهان فيرما نحو 6 مليارات من tokens المخرجات، وعدة محاولات فاشلة قبل أن تحافظ منصة تنسيق، هي Prove2Me، على انتظام عمل الوكلاء. وإعادة التحقق أرخص بكثير من المراجعة اليدوية، لكنها ليست هيّنة: فوفقًا للمستودع، استغرق تصريفه خمس ساعات ونصفًا مع 96 عملية متوازية، واستغرق Comparator قرابة خمس عشرة ساعة مع ذروات بلغت 230 غيغابايت من الذاكرة.

التقسيم نفسه، خارج الرياضيات

ما ينظّمه Lean للرياضيات يُستخدم بالفعل لبرمجيات في بيئة الإنتاج.

في AWS، يحتفظ فريق Cedar، وهي اللغة التي تُكتب بها سياسات التفويض (من يستطيع أن يفعل ماذا وعلى أي مورد)، بنموذج لكل مكوّن في Lean، أصغر بنحو عشر مرات من الكود الفعلي المكتوب بـRust. ويبرهن على خصائص أمنية على هذا النموذج، ويولّد ملايين المدخلات العشوائية ليتحقق من أن النموذج والكود يعطيان الجواب نفسه. ووفقًا لدراسة الحالة التي نشرها Lean، لا يصدر أي إصدار جديد من Cedar ما لم يكن النموذج والبراهين وتلك الاختبارات محدَّثة.

في Microsoft، تكتب SymCrypt، مكتبة التشفير التي يستخدمها Windows وAzure، خوارزمياتها الجديدة بـRust، وتترجمها إلى Lean بأداة تُسمّى Aeneas، وتبرهن على أنها تستوفي مواصفات مشتقة من معايير NIST. وفي يوليو نشرت أولى البراهين الكاملة: ML-KEM، وهي خوارزمية لتبادل المفاتيح مقاومة للحواسيب الكمومية، وSHA-3. ويقسّم المخطط الذي يشرحون به ذلك العمل إلى ثلاثة أقسام. وكلاء الذكاء الاصطناعي، الذين يصفونهم بأنهم احتماليون، يكتبون البراهين. والأدوات، وهي حتمية، تُصرِّف وتترجم وتتحقق. ويكرّس البشر انتباههم لمراجعة كيفية صياغة المعايير صياغة رسمية وأي الخصائص مهمة.

هذا التقسيم هو أكثر ما يمكن نقله من Lean إلى أي فريق يُدخل الذكاء الاصطناعي في عملية ما، حتى لو لم يكتب برهانًا قط. يمكن أن يكون التوليد وفيرًا وقليل الموثوقية إذا تحققت ثلاثة شروط. أن يكون ما يتحقق صغيرًا وحتميًا ومستقلًا عمّا يولّد. وأن يُعرف بالضبط ما افتُرض مسبقًا، أي ما يعادل #print axioms: أي الاختبارات جرى تخطيها، وما الذي جرت محاكاته، وما الذي قُبل دون مراجعة. وأن يراجع البشر المواصفات، وهي الجزء الذي لا تستطيع أي آلة أن تتحقق منه نيابةً عنهم. فالاختبارات وأنظمة الأنواع نسخ ضعيفة من الفكرة نفسها؛ وLean نسختها القصوى.

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

المصادر

• Anthropic: «Formalizing Fermat’s Last Theorem»، 4 سبتمبر 2026 ومستودع anthropics/fermats-last-theorem، جرى الاطلاع عليه في 8 أكتوبر 2026.
• Trail of Bits: «A “proof” of Fermat’s Last Theorem that fits the margin»، 9 سبتمبر 2026.
• ليوناردو دي مورا: تحليل خلل النواة رقم 14576، 1 أغسطس 2026 وملاحظات إصدار Lean 4.32.2، 28 يوليو 2026.
• con-leche: مدقق خارجي لـLean مع برهان على الاتساق وLean Kernel Arena.
• مجتمع Lean: «Did you prove it?» وإحصاءات Mathlib، جرى الاطلاع عليهما في 8 أكتوبر 2026.
• Lean FRO: التاريخ والتنظيم والدليل المرجعي لـLean: «Validating a Lean Proof».
• Hubert et al.: «Olympiad-level formal mathematical reasoning with reinforcement learning»، Nature، نوفمبر 2025.
• Lean: حالة Cedar في AWS وAWS Open Source Blog: «Lean into verified software development».
• Microsoft Research: «Verifying Rust cryptography in SymCrypt, from standards to code»، 13 يوليو 2026.
• جُرّبت أمثلة الكود الخاصة بنا على محرر Lean الرسمي على الويب بالإصدار v4.35.0-rc4.