بوانكاريه، تتحقق منه آلة سطرًا بسطر

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

برهان مكثّف، ومكتبة ناقصة

تنص حدسية بوانكاريه، التي برهنها بيرلمان، على أن كل متعدد شعب ثلاثي الأبعاد مغلق وبسيط الترابط — أي بشكل غير رسمي، فضاء ثلاثي الأبعاد منتهٍ لا ثقوب فيه يمكن أن تعلق بها أنشوطة — مكافئ للكرة ثلاثية الأبعاد. ويتبع البرهان برنامج تدفق ريتشي الذي أطلقه ريتشارد هاميلتون. وقد قدّمت أوراق بيرلمان الأولية الثلاث في 2002–2003 الحجج الأساسية بصيغة شديدة التكثيف؛ ثم تلتها عروض مفصلة، منها دراسة جون مورغان وغانغ تيان عام 2007 التي يسير عليها هذا المشروع.

يعتمد ذلك البرهان على تحليل هندسي كانت مكتبة Lean المجتمعية، Mathlib، تفتقر إليه إلى حدٍّ بعيد. وكان لا بد من بناء جزء كبير من الأسس من الصفر.

معالم جمّدها الرياضيون

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

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

ثم عمل الوكلاء بالتوازي، عبر جلسات تفاعلية مع أدوات برمجة — أساسًا Codex وClaude Code — وعبر نظام يُدعى Archon Horizon يوزّع “مهمات” محددة النطاق على خوادم كثيرة. وكان روبوت برمجي يُصرّف كل مساهمة ويدمج المقبولة منها. وتولّى GPT-6-Astra معظم صياغة العبارات وبناء البراهين؛ واستُخدم Fable-5.1 للفحوص المستقلة، وتشخيص المهام المتعثرة، ومراجعة العبارات.

2.8 مليون سطر في نحو أسبوعين

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

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

ما الذي ظل البشر يفعلونه

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

مُتحقَّق منه، لكنه لم يُرتَّب بعد

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

تضارب المصالح. استخدم الفريق Claude Code والنموذج Fable-5.1، وكلاهما من Anthropic، إلى جانب GPT-6-Astra، المستخدَم عبر اشتراكات OpenAI، والذي أنجز معظم العمل. كما تقارن الورقة مشروعها بالصياغة الصورية لمبرهنة فيرما الأخيرة التي أجرتها Anthropic. وهذا المقال كتبه Claude.