ناشئة صينية تحول موسوعة رياضية إلى كود متحقق بذكاء اصطناعي

في 11 نوفمبر، أعلنت شركة أكسيوم ماث، الناشئة المتخصصة في الذكاء الاصطناعي والرياضيات، أنها حولت مشروع ستاكس، مرجع مفتوح في الهندسة الجبرية استغرق إعداده نحو عشرين عاماً وشارك فيه أكثر من 650 رياضياً، إلى حزمة أكواد قابلة للتحقق الآلي بلغة ليان. ويقدم المشروع، الذي أسسه عالم الرياضيات يوهان دي يونغ في جامعة كولومبيا منذ عام 2005، أكثر من 20 ألف تعريف ومقولة ومبرهنة، موزعة على 116 فصلاً ونحو 7600 صفحة، ويعتمد بنية شديدة التنظيم تسمح بتتبع اعتماد أي نتيجة على نتائج أخرى عبر مراجع قصيرة. ووفق الشركة، يضم المستودع الجديد، المبني على مكتبة ماتليب الرياضية المفتوحة والمراجَعة يدوياً، نحو 15,750,000 سطر، ويغطي جميع عناصر ستاكس التي يمكن تمثيلها رسمياً، باستثناء ما رُفضت ترجمته لعدم ملاءمته أو ما صنف كمهمات مفتوحة. واعتمدت أكسيوم نهجاً يمزج هندسة البرمجيات بوكلاء الذكاء الاصطناعي، فخصصت وكلاء للمهمة المعمارية، وآخرين لصياغة التعريفات، وفريقاً لإثبات النتائج. وكشفت العملية عن عشرات التصحيحات المحتملة في الكتاب الأصلي، وأنتجت مضاداً في حالات لم تصمد فيها مقترحات. ولم تكن هذه الخطوة حدثاً معزولاً؛ فخلال 2025 أنجزت الشركة صياغة رسمية لنظرية الفجوات الأولية، بما في ذلك نتيجة متعلقة بالفجوة 246 المرتبطة بعمل تشانغ ييتانغ، ولاحقاً عملت على إثبات تصنيف الزمر البسيطة المنتهية الضخم الممتد عبر جيل من الرياضيين. غير أن تحويل مرجع حي كستاكس يعكس تحولاً في مجال الصياغة الرياضية الآلية: من إثبات نظرية مفردة إلى بناء قاعدة معرفية متجددة يمكن للباحثين والذكاء الاصطناعي استخدامها والتحقق منها تدريجياً. وقسمت أكسيوم الأكواد إلى نواة أساسية تحقق منها فريق يتألف من أربعة رياضيين وفق معايير ماتليب، وطبقة أمامية كتبها الوكلاء وتنتظر مراجعة بشرية قبل نقلها. ويبقى فحص كل برهان داخل ليان شرطاً للسلامة المنطقية، لا لضمان تطابق المعنى الرياضي. كما ستبقى النسخة منفصلة عن المستودع الأصلي، بعد تحذير دي يونغ من إدخال التعليقات والطلبات الناتجة عن الذكاء الاصطناعي مباشرة. وترى الشركة أن هذا العمل يختبر ما إذا كان الكود المولَّد آلياً قادراً على الصمود أمام التدقيق وإنتاج بنية رياضية قابلة لإعادة الاستخدام، في ظل نقاش متزايد داخل مجتمع ليان بشأن القيمة العملية للأكواد الضخمة. وقد أظهرت تجارب أخرى قدرة نماذج الذكاء الاصطناعي على إنتاج ملايين الأسطر في فترات قصيرة، لكن متخصصين يشيرون إلى أن الفائدة تتحقق فقط إذا خضعت للأبحاث البشرية، واتبعت قواعد المكتبة، ونسجت مع المعارف القائمة. وعلى المدى الطويل، قد تصبح هذه المكتبات المدققة مادة موثوقة لتوسيع البراهين، ومصدراً لمراجعة أسرع، وأداة تكشف الثغرات الخفية في النقاش الرياضي، لكنها تبقى اليوم محكومة بقدرات المراجعة البشرية.