يبدو أن الذكاء الاصطناعي يحل كل أسبوع مشكلة رياضية جديدة. في الشهر الماضي، أصدرت OpenAI وحدها 719 ورقة بحثية تدّعي حلها لأصعب المشكلات في هذا المجال. حتى فحص الحاسوب قد يخطئ. بعد سنوات من محتوى الذكاء الاصطناعي غير المفيد، لا يمكن للمرء إلا أن يتساءل: هل ستكون الرياضيات المجال التالي المتأثر؟
يمكن لـ AxiomMath تجنب هذا المصير ليس عن طريق إبطاء الوتيرة، بل ببناء أساس أكثر متانة. تهدف هذه الشركة الناشئة المُقيَّمة بقيمة 1.6 مليار دولار إلى إنشاء طبقة أساسية مُوثَّقة، يمكن للوكلاء الذكاء الاصطناعي الاعتماد عليها لكتابة البرمجيات، وفي النهاية ممارسة الأبحاث العلمية.
في الأربعاء، أعلنت الشركة أنها تحقق رسميًا مشروع Stacks، وهو أحد أكبر الإنجازات الرياضية التي كتبها البشر. يُقدّر الرياضيون مشروع Stacks بشكل عالٍ جدًا. ووصف بيتر ووت، أستاذ الرياضيات في جامعة كولومبيا، المشروع بأنه "لا يوجد شيء آخر يقارن به تقريبًا"، وقارن المشروع بـ"سلسلة Bourbaki الشهيرة" — وهي السلسلة التي أعادت بناء الرياضيات من الأساسيات خلال القرن العشرين.
بدأ زميل وويت الكولومبي، جوهان دي يونغ، مشروع Stacks في عام 2005 كمرجع مفتوح المصدر. منذ ذلك الحين، قدم الرياضيون مساهمات له، ممتدّين من الجبر على مستوى الجامعة إلى أفكار متقدمة في الجبر والهندسة ونظرية الأعداد.
ترجمت مجموعة الوكلاء الذكاء الاصطناعي للشركة قاعدة البيانات المكونة من حوالي 7,654 صفحة إلى حوالي 16 مليون سطر من الكود القابل للتحقق بواسطة الحاسوب.
الهدف من الرياضيات الرسمية هو ضمان موثوقية بنيتها الأساسية. يقوم الرياضيون بإعادة كتابة الإثباتات بلغة برمجة تُسمى Lean، ثم يتحقق برنامج يُعرف باسم مساعد الإثبات من هذه الكودات سطرًا بسطر. إذا نجح الإثبات، يمكن للرياضيين الوثوق بأنه صحيح من الناحية المنطقية.
يستخدم المهندسون نفس الفكرة، أي التحقق الرسمي، للتحقق من جدوى تصميم الرقائق؛ بينما استخدم الباحثون الفرنسيون هذه الطريقة لاكتشاف ثغرة في برنامج حساب الإعانات الأسرية.
بالنسبة لمثل مشروع Stacks، فإن التحقق من كل نظرية على حدة هو مجرد جزء من العمل. في Stacks، تكون النظريات والتعريفات مترابطة، وكل منها يبنى على ما سبقه. مثل شجرة عائلية، يمكن تتبع العديد من النتائج في Stacks إلى نتائج أقدم.
هذا الترابط جعل Axiom غير متأكد في البداية مما إذا كان المشروع قابلاً للتنفيذ. كان على الفريق الحفاظ على سلامة جميع الروابط داخل حوالي 16 مليون سطر من كود Lean.
قال المدير التنفيذي لشركة Axiom، كارينا هونغ، لـ TechCrunch: "الحجم الكبير والدقة عادةً لا يتوافقان في الواقع. [Stacks] هي مجموعة من النتائج الرياضية التي تشكل الأساس الرياضي. ترغب في أن تكون [النظريات] متسقة مع بعضها البعض، وليس متناقضة مثل المفارقات. كما ترغب في أن لا تتعارض هذه التعريفات مع بعضها البعض."
كان هذا المدير التنفيذي البالغ من العمر 25 عامًا قد ترك برنامج الدكتوراه في الرياضيات من جامعة ستانفورد، وأسس الشركة في مارس 2025. وفي مارس من هذا العام، أكملت Axiom جولة تمويل من الفئة A بقيمة 200 مليون دولار بقيادة Menlo Ventures.
هونغ قال: "لم نكن متأكدين في ذلك الوقت مما إذا كان يمكن لـ vibe coding الحفاظ على جمال Stacks."
لإكمال هذا المشروع، حدد الفريق هيكلًا مرنًا للوكلاء وسمح لهم بالعمل بالتوازي. كما قال أشفين سواميناثان، عضو فريق تقنية Axiom: "بالنسبة لـ Stacks، حددنا هرمًا... لكنه ليس هرمًا يحدد بدقة ما يجب على كل وكيل فعله. فالوكلاء يبحثون عن المهام بأنفسهم ويحددون الأمور التي يمكن معالجتها بالتوازي."
كما درّب Axiom نماذجه الخاصة لجعلها متميزة في الرياضيات. يقول هونغ إن هذا النهج هو ما لم تتبعه معظم شركات التحقق الناشئة الأخرى. في البداية، اعتمد الفريق على خبير داخلي في منهجية Lean لتعليم الوكلاء تكوين معايير قرار مشابهة لتلك البشرية. ومع مرور الوقت، يقول هونغ، تعلم الوكلاء هذه القدرة بأنفسهم.
هذا الإنجاز يملأ أحد أكبر الفراغات في الرياضيات الرسمية. يقول سواميناثان: "عندما تنظر إلى المحتوى الرياضي الذي تم ترسيخه بالفعل، ستجد ثقبًا أسود هائلًا. وهذا الثقب الأسود يغطي الهندسة الجبرية."
قال سواميناثان: "حتى الآن، كان الباحثون الذين يرغبون في استخدام Lean للتحقق من أعمال جديدة في الهندسة الجبرية لا يمتلكون سوى القليل جدًا من الأساسيات الجاهزة. "الآن لديهم ذلك."
تعتقد Axiom أن كل نتيجة مُوثَّقة تصبح ككتلة بناء، ويمكن للإثباتات المستقبلية أن تُبنى على الرياضيات التي تم التحقق منها مسبقًا دون الحاجة إلى البدء من الصفر. وخلص الرياضي من جامعة كاليفورنيا في لوس أنجلوس وحاصل جائزة فيلدز، تيرينس تاو، إلى هذه النقطة بعبارة أكثر إيجازًا: "كلما امتلكت إثباتات مُصاغة أكثر، استطعت إنشاء إثباتات مُصاغة أكثر."
الجمهور المستهدف لـ Axiom لا يقتصر على الرياضيين. فقد سعى المطورون لفترة طويلة لضمان خلو كودهم من الثغرات والمخاطر الأمنية. ومع كتابة وكلاء الذكاء الاصطناعي لعدد متزايد من البرمجيات، سيصبح هذا المشكل أكبر فقط.
Axiom رهان، ستتطلب البرمجيات المستقبلية بناءً على أساس مُثبت، مثل Stacks الحالي.
قال سواميناثان: "نعتقد أن الرياضيات هي المجال الذي تبدأ فيه بناء هذه الأشياء، وهي مهارة قابلة للنقل. يمكن للوكلاء قراءة كودنا وفهمه وبناء بنية تحتية جديدة عليه. إن التصيير الذي قمنا به باستخدام Lean هو الآن الأساس الأساسي الذي يمكن للوكلاء البناء عليه."
الطريقة التي يبني بها Axiom وكيلًا لـ Stacks — العمل بالتوازي واختيار المهام بنفسه — هي بالضبط الطريقة التي تتوقعها هونغ أن تصبح شائعة في العديد من وظائف الذكاء الاصطناعي في المستقبل. وهي ترى أن وكلاء الذكاء الاصطناعي يحتاجون إلى قاعدة معرفة منظمة وقابلة لإعادة الاستخدام لتجنب إنتاج محتوى عديم القيمة.
هونغ يقول: "أنت ترغب في أن يمتلك [الوكيل] قاعدة بيانات قابلة لإعادة الاستخدام، يمكنه البناء عليها ودفع الحدود باستمرار. إذا قمت في البداية بملئها باختيارات هندسية سيئة، فسيصبح من الصعب جدًا توسيع تلك الحدود."
هونغ واثقة جدًا من هذه الطريقة، بل وقدمت تحديًا علنًا. قالت: "أنا أتحدى جميع شركات البرمجة لتنفيذ هذا النوع من العمل التشكيلي على هذا الحجم."