في زمنٍ تتطور فيه تقنيات الذكاء الاصطناعي بوتيرة غير مسبوقة، تظهر الابتكارات الحديثة التي تمزج بين التفكير الرياضي والاستدلال الرسمي كخطوة ثورية نحو حل المشكلات الرياضية المعقدة. تقدم دراسة جديدة إطارًا آليًا يجمع بين الاستدلال الطبيعي (Natural Language Reasoning) والتحقق الرسمي (Formal Verification) لمواجهة التحديات في حل مسائل رياضية بحثية.

يتكون هذا الإطار من عنصرين رئيسيين: الوكيل الذي يقوم بالاستدلال غير الرسمي، المعروف باسم Rethlas، ووحدة التحقق الرسمي، Archon. يقوم Rethlas بدمج أساليب الاستدلال مع محرك البحث الخاص بالنظرية، Matlas، لاستكشاف استراتيجيات الحل وإعداد براهين مرشحة. بينما يتولى Archon، المجهز بأداة LeanSearch، تحويل الحجج غير الرسمية إلى مشاريع Lean 4 مصدقة من خلال التحليل التدريجي والتنقيح الآلي، مما يضمن صحة النتائج بطريقة يمكن التحقق منها.

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

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