FormalFlow يستخدم الذكاء الاصطناعي بإشراف بشري لصياغة مبرهنة تدعم MIP* = RE
تعرض ورقة أولية صدرت في 17 سبتمبر برهاناً بلغة Lean 4 لمبرهنة أساسية في السلامة الكمية، طُوّر خلال 63 يوماً.
جعل البرهان الطويل قابلاً للتحقق
تخوض الصياغة الصورية بمساعدة الذكاء الاصطناعي اختباراً جديداً على مستوى البحث. يقدم سيروي لو ورويشوان دنغ ويانتشياو تشو وتشنغفنغ جي في ورقة أولية بتاريخ 17 سبتمبر نظام FormalFlow، الذي ينسق وكلاء البرهان حول خطة مشتركة بإشراف بشري.
يعلن الفريق إكمال برهان بلغة Lean 4 للسلامة الكمية للاختبار الكلاسيكي للدرجة الفردية المنخفضة خلال 63 يوماً. وهذه مبرهنة داعمة لنتيجة MIP* = RE؛ ولا يشمل المشروع الصياغة الصورية للنتيجة كاملة.
وتبرز التجربة صعوبة عملية: قد تجتاز الشيفرة الفحص البرمجي مع أنها تمثل ادعاءً رياضياً غير المقصود. لذلك تراجع العملية المتكررة اعتماد البراهين بعضها على بعض ومعنى العبارات. ويذكر المؤلفون أنهم صححوا افتراضات وأخطاء وسيطة مع الحفاظ على حد الخطأ النهائي المنشور وفق الافتراضات المصححة.
تكمن القيمة للبحث الرياضي في إتاحة برهان يمكن للآخرين فحصه والتحقق منه. وهذه نتائج ورقة أولية؛ ولم تُعِد MathsAI بناء المكتبة المنشورة للتحقق منها بصورة مستقلة.