Axiom يحل مسألة رياضية غير محلولة ويكتب برهاناً موثقاً
أعلنت شركة Axiom عن إنجاز غير مسبوق، حيث تمكن وكيلها الذكي AxiomProver من حل مسألة رياضية مفتوحة وكتابة برهان رسمي مكتمل التحقق في Lean، دون أي تدخل بشري، ما يمثل أول مرة يحدث فيها هذا في أبحاث الرياضيات المتقدمة.
تفاصيل الخبر
حقق AxiomProver، نظام الذكاء الاصطناعي المخصص للرياضيات، خطوة تاريخية بحل مسألة Fel المفتوحة حول syzygies لمجموعات عددية، مع إنتاج برهان رسمي كامل.
- حل المسألة تم بشكل مستقل دون أي توجيه بشري، من صياغة المشكلة بلغة طبيعية إلى إخراج ملف Lean صحيح.
- المسألة المختارة تتطلب قدرات عالية مثل تحليل هرمي معقد، القدرة على الرجوع إلى الوراء، وتحويل التعريفات تلقائياً إلى صياغة رسمية.
- Fel يوفر صيغة مغلقة لمتغيرات syzygy في مجموعات عددية، وتقع في تقاطع نظرية الأعداد المضافة والجبر التبادلي، وهي مجالات أساسية في أبحاث الرياضيات.
- البرهان يستخدم متغيرات متعددة تشمل متعددات الحدود العالمية Tₙ، المرتبطة أيضاً بأعمال Ramanujan في دفتره المفقود.
- AxiomProver هو نظام Verified AI تحت التطوير، ويهدف لأن يكون “رياضي الذكاء الاصطناعي” الأول الذي يشارك في أبحاث متقدمة.
- النتائج متاحة على arXiv كمقالة أولية، مع كود Lean على GitHub لتأكيد البرهان والتحقق منه.
الأهداف المستقبلية
Axiom ترى هذا الإنجاز كبداية لسلسلة من أبحاث الذكاء الاصطناعي في الرياضيات المتقدمة.
- تطوير النظام ليتمكن من التعامل مع مسائل بحثية أكثر تعقيداً بشكل مستقل.
- توسيع قدرة AxiomProver على التعامل مع مختلف فروع الرياضيات النظرية.
- تمكين الباحثين من تقديم أسئلتهم البحثية بصيغة LaTeX ليتم حلها تلقائياً.
- نشر سلسلة أوراق بحثية جديدة تعكس مساهمة الذكاء الاصطناعي في بناء نظريات رياضية جديدة.
يمثل هذا الإنجاز لحظة فارقة في تاريخ الذكاء الاصطناعي والرياضيات، حيث يثبت أن الأنظمة الذكية يمكنها المساهمة في الاكتشافات النظرية بشكل مستقل وموثوق.
