Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem

ملخص تقني: دراسة حالة صياغة مسألة "الجراد" باستخدام واجهة أرسطو البرمجية (Aristotle API)

بيان المسألة
تقدم هذه الورقة دراسة حالة لصياغة مسألة "الجراد" (Grasshopper problem)، والتي طُرحت أصلاً كالمسألة السادسة في أولمبياد الرياضيات الدولي الخمسين (IMO 2009). تنص المبرهنة على أنه لأي مجموعة من $n$ من الأعداد الصحيحة الموجبة المتمايزة $\{a_1, \dots, a_n\}$ ومجموعة $M$ من $n-1$ من الأعداد الصحيحة الموجبة (حيث المجموع الكلي $\sum a_i \notin M$)، توجد تبديلة (permutation) $\sigma$ للقفزات بحيث لا يقع أي مجموع جزئي وسيط $S_k = \sum_{i=1}^k a_{\sigma(i)}$ ضمن المجموعة $M$. وتُلاحظ المسألة بصعوبتها التاريخية، حيث سجلت أدنى متوسط درجات بين جميع مسائل أولمبياد الرياضيات الدولي لعام 2009، وتتطلب استدلالاً توافقياً (combinatorial reasoning) غير بديهي يتضمن التبديلات والمجموعات المحظورة.

المنهجية
تستخدم الدراسة واجهة أرسطو البرمجية (Aristotle API)، وهي نظام آلي لإثبات المبرهنات يجمع بين البحث الموجه بالنماذج اللغوية، وتوليد التمهيدات (lemmas) غير الرسمية، والصياغة الرسمية داخل مساعد الإثبات Lean 4 (باستخدام Mathlib). قدم المؤلفون أمراً (prompt) محدداً لواجهة أرسطو البرمجية يطلب إثباتاً دقيقاً وكاملاً لمسألة الجراد، مع منع الاستشهاد بالمسألة كمبرهنة معروفة صراحةً، والمطالبة ببناء تبديلة صالحة.

الناتج هو أثر (artefact) من مشروع Lean 4 يحتوي على نسخة معممة من المبرهنة (تسمح بأن يكون $|M| < n$ بدلاً من $n-1$ حصراً، وتسمح بأن يكون $0 \in M$). قام المؤلفون بإجراء فحص دقيق للكود المولد للتمييز بين التصريحات (declarations) التي تم التحقق منها آلياً بالكامل، وتلك التي تحتوي على أماكن شاغرة غير محلولة للإثبات (sorry).

النتائج الرئيسية والمكونات المتحقق منها
لم ينتج التطوير المولد بـ Lean عملية إثبات كاملة للمبرهنة الرئيسية. بدلاً من ذلك، نتج عنه أثر هجين يتكون من أربع تمهيدات مساعدة متحقق منها بالكامل ومبرهنة رئيسية واحدة غير محلولة:

1. المكونات المحلية المتحقق منها:

   • PS last: تحقق من أن المجموع الجزئي الأخير يساوي المجموع الكلي للقفزات.
   • PS swap: تحقق من أن التبديل المتجاور للقفزات يؤثر فقط على المجموع الجزئي الوسيط المحدد في ذلك الموضع، تاركاً غيره دون تغيير.
   • PS swap eq: تحقق من الشكل الجبري للمجموع الجزئي المتغير بعد التبديل ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$).
   • maximizer swap in M: تحقق من حجة عظمى محلية (local maximality argument). وهي تثبت أنه إذا كانت تبديلة ما تعظم دالة نتيجة (score function) محددة $G(\sigma)$، وكان مجموع جزئي في موضع قابل للتبديل ينتمي إلى $M$، فإن القيمة الناتجة عن التبديل يجب أن تنتمي أيضاً إلى $M$.

2. المكون العالمي غير المحلول:

   • المبرهنة الرئيسية، grasshopper، أُغلقت مباشرة بواسطة sorry واحدة.
   • يحدد ملخص مخرجات أرسطو الخطوة المفقودة بأنها حجة عدّ عالمية (global counting argument). بينما تثبت التمهيدات المحلية أن عمليات تبديل محددة تفرض الانتماء إلى $M$، فشل النظام في تنسيق هذه الحقائق لإثبات أنها تولد على الأقل $n$ من القيم المحظورة المتميزة، مما قد يناقض الافتراض بأن $|M| < n$. لا يختزل كود Lean المبرهنة الرئيسية إلى تمهيد عد منفصل ومُرمز؛ بل تظل الفجوة التزاماً غير مُثبت.

المساهمات
تقدم الورقة مساهمتين رئيسيتين:

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

الأهمية والادعاءات
تجادل الورقة بأن التمييز بين "التصريحات المتحقق منها" و"التصريحات المغلقة بـ sorry" أمر بالغ الأهمية لتفسير الإثبات المدعوم بالذكاء الاصطناعي. تكمن أهمية دراسة الحالة هذه في إثباتها أن البحث المحلي عن الإثبات يمكن أن ينجح بينما يظل الاستدلال العالمي دون حل.

يؤكد المؤلفون أن نجاح تجميع (compilation) ملف Lean يحتوي على sorry ليس دليلاً كافياً على اكتمال الإثبات. يعمل الأثر كنموذج تحذيري: بينما يمكن لأدوات الذكاء الاصطناعي توليد تطورات رياضية جوهرية ومتحقق منها (مثل التمهيدات الأربعة المساعدة)، إلا أنها قد تترك المحرك المنطقي الأساسي للإثبات (التناقض العالمي) دون تنفيذ. وتخلص الورقة إلى أن الصياغة الرسمية الموثوقة المدعومة بالذكاء الاصطنا_ت تتطلب فحصاً دقيقاً لالتزامات الإثبات وتبعياتها، بدلاً من الاعتماد على مجرد وجود الكود المولد.