Axiom تنشر صياغة رسمية بلغة Lean لمشروع Stacks كاملًا، نحو 16 مليون سطر أنجزتها أسراب من وكلاء الذكاء الاصطناعي
أصبح المرجع في الهندسة الجبرية المؤلف من نحو 7500 صفحة مكتبة واحدة مُتحقَّقًا منها آليًا؛ ولم يراجع رياضيون مستقلون بعد مدى أمانة الصياغات.
لماذا يهم
لم تكن للهندسة الجبرية الحديثة بنية تحتية تُذكر في Lean، لأن برهانًا واحدًا قد يعتمد على سلاسل طويلة من النتائج في الجبر التبديلي والمخططات والحزم والكوهومولوجيا. وتقول Axiom إن مكتبتها تحافظ على الوسوم الدائمة لمشروع Stacks، بحيث يستطيع البشر ووكلاء الذكاء الاصطناعي استيراد تعريفاتها ومبرهناتها مباشرة في براهين جديدة. ويأتي ذلك بعد صياغة Axiom الرسمية بلغة Lean لتصنيف الزمر البسيطة المنتهية في 27 أكتوبر 2026. ويبقى أن نرى هل سيجد الرياضيون الذين يقارنون الصياغات بالنص الأصلي أنها أمينة، وهل ستُعتمد المكتبة إلى جانب Mathlib.
حقائق رئيسية
- مشروع Stacks: نحو 7500 صفحة
- نحو 16 مليون سطر من شيفرة Lean
- أُنجز بأسراب منسقة من وكلاء الذكاء الاصطناعي
- أطلقه Johan de Jong من جامعة كولومبيا عام 2005
- متاح على stacks.axiommath.ai
- يلي صياغة Axiom لتصنيف CFSG في 27 أكتوبر 2026