الذكاء الاصطناعي لشركة Axiom Math يتحقق من نظرية فجوات الأعداد الأولية 246 في Lean

تقول Axiom Math إن نظام AxiomProver الخاص بها أنتج برهانًا مُتحققًا آليًا في Lean 4 لأقوى نتيجة معروفة حول الفجوات بين الأعداد الأولية: النظرية التي تنص على وجود أزواج لا نهائية من الأعداد الأولية تختلف عن بعضها بأكثر من 246. نشرت الشركة النتيجة في 17 أغسطس 2026 كخريطة توثيق تفاعلية تُنسب إلى 41 مساهمًا مسمى في الرياضيات والهندسة والباحثين الرئيسيين، مع IEEE Spectrum أولاً تقارير عن هذا الإنجاز.

الحد 246 هو الحد الحالي للمعرفة البشرية في الهجوم الطويل على فرضية أزواج الأعداد الأولية المتطابقة، الفرضية التي صاغها ألفونس دو بولينياك في القرن التاسع عشر ولا تزال غير مثبتة. تصف صفحة مشروع Axiom Math العمل بأنه توثيق موحد لورقة جيمس ماينارد عام 2013 “فجوات صغيرة بين الأعداد الأولية” إلى جانب الجزء المتبع من تعاون Polymath8b الذي خفض حد ماينارد من 600 إلى 246. تُنظم البراهين المُتحققة آليًا في مكتبة Lean عامة تُدعى PrimeGapsLib، مع نظرية 246 كنتيجة رائدة لها.

“هذه النظرية تمثل حاليًا عتبة المعرفة البشرية حول الأعداد الأولية”، قال كين أونو، الرياضي المؤسس في Axiom Math.

التحقق الرسمي يعني ترجمة برهان إلى لغة يمكن لبرنامج صغير موثوق يُسمى النواة فحصه سطرًا بسطر. النتيجة ليست ضمانًا مطلقًا — فالنص نفسه يجب أن يُترجم بدقة، ويجب أن يكون الفاحص موثوقًا — لكنها تُزيل قابلية الخطأ البشري من السلسلة. حتى الآن، تم قياس أنظمة الذكاء الاصطناعي التي تتنافس في معايير الرياضيات غالبًا على مسائل مسابقات ذات براهين قصيرة ومستقلة؛ الفجوة بين تلك النتائج وتوثيق المستوى البحثي كانت واسعة، وهو نمط ظهر في أنظمة سابقة تفوقت في هندسة الأولمبياد بينما تركت الرياضيات البحثية إلى حد كبير دون لمس.

من 70 مليون إلى 246

الفرضية نفسها، التي صاغها ألفونس دو بولينياك بدقة في القرن التاسع عشر، لا تزال غير مثبتة. أول حد محدود من أي نوع ظهر في 2013، عندما أثبت ييتانغ تشانغ أن أزواجًا لا نهائية من الأعداد الأولية تقع ضمن 70 مليون من بعضها البعض. بعد أشهر، قدم ماينارد طريقة منخلية مُحسّنة وخفض الحد إلى 600 — عمل ساهم في حصوله على ميدالية فيلدز 2022 — ودفع تعاون Polymath8b، الذي شمل ماينارد وتيرنس تاو، الحد إلى 246. توضح خريطة Axiom Math هذه السلسلة كالمشروع الذي سعت إلى توثيقه.

يتبع التوثيق خط أنابيب تصفه الشركة في ثلاث مراحل. أولاً يكتب الباحثون البرهان كخريطة — كل تعريف، لمَّة، ونظرية تُعطى تسمية، وصياغة دقيقة، وقائمة بالنتائج التي تعتمد عليها — منتجين رسمًا بيانيًا للاعتمادية يرتب العمل. ثم يولد AxiomProver، نظام الشركة متعدد الوكلاء للبحث الرياضي عبر البرهان الرسمي، براهين Lean 4 قابلة للتحقق آليًا مبنية على Mathlib، مكتبة الرياضيات المجتمعية، وعلى مشروع PrimeNumberTheoremAnd، التوثيق القائم بقيادة أليكس كونتوروفيتش وتاو. بعد ذلك يراجع فريق Axiom الشيفرة المولدة وينظمها في PrimeGapsLib.

تتجاوز النتائج الرئيسية المعلن عنها في المكتبة قليلاً ما هو العنوان الرئيسي. إلى جانب حد 246، تُوثق المكتبة حد 600 لماينارد، وتضم تحديًا للتحقق ذاتيًا — مبنيًا فقط على Mathlib، مع ترك خانة البرهان فارغة — يتيح لأي شخص يمتلك أداة المقارنة Lean أن يؤكد بشكل مستقل أن براهين المكتبة تتطابق مع النظريات المعلنة. تحذر الشركة من أن الفحص الكامل قد يستغرق ساعات؛ نسخة مُختصرة تغطي النتيجتين الأخريين تُنجز في دقائق.

أين يقع هذا بين ادعاءات التحقق الرسمي للذكاء الاصطناعي

تظهر النتيجة في عام تشهد فيه ادعاءات متصاعدة حول أنظمة الذكاء الاصطناعي التي تقوم بالرياضيات على مستوى البحث، معظمها مرتبط بنتائج مسابقات أو براهين قصيرة. كانت Axiom Math واحدة من أكثر المطالبين عدوانية: يُنسب إلى AxiomProver حل مشكلات كانت مفتوحة سابقًا، بما في ذلك أعمال نشرتها الشركة في مجلات محكمة، وقد حلّت أنظمة الذكاء الاصطناعي الآن عدة مشكلات إردوش طويلة الأمد. توثيق 246 هو نوع مختلف من النتيجة — ليس نظرية جديدة، بل إعادة بناء مُتحققة آليًا لأحد أكثر البراهين تعقيدًا في نظرية الأعداد الحديثة.

أقرب مقارنة كانت في وقت سابق من هذا العام، عندما استخدمت Math, Inc. وكيلها Gauss لإكمال البرهان الرسمي لنتائج تعبئة الكرات التي فازت بها ماريينا فيازوفسكا بجائزة ميدالية فيلدز في البُعدين 8 و24. سيدهارت هاريهاران، طالب الدكتوراه في جامعة كارنيجي ميلون الذي قاد جهود الخريطة البشرية لتلك التوثيق وهو الآن متدرب في Axiom Math ومساهم رياضي مسمى في مشروع 246، يجادل بأن النتيجة الجديدة هي الإنجاز الأكثر شمولًا. وفقًا لتفسيره، فإن Axiom بُني لإعادة الاستخدام: بدلاً من توثيق لمرة واحدة لبرهان واحد، تُعد PrimeGapsLib مكتبة مُصانة لنتائج فجوات الأعداد الأولية تهدف إلى دعم أعمال وتوثيقات مستقبلية.

هذا التمييز مهم لكيفية قراءة النتيجة. تُظهر عملية تحقق لمرة واحدة أن النظام يمكنه الصمود أمام برهان صعب واحد. تُظهر مكتبة شيء أقرب إلى البنية التحتية — آلية رسمية قابلة لإعادة الاستخدام يمكن للنتائج الأخرى البناء عليها — وهو الاتجاه الذي تتبعه أنظمة البرهان الرسمي بينما تتحول من حل تمارين إلى فحص رياضيات حقيقية. تستند ادعاءات القدرة هنا إلى أدوات عامة وقابلة لإعادة التشغيل بدلاً من درجة معيارية: الخريطة، شفرة Lean، وتحدي المقارنة المصمم بحيث يتمكن الباحثون الخارجيون من التحقق من البراهين بأنفسهم.

يُصوّر أونو الرياضيات كمنصة اختبار لطموح أكبر. إذا كان بالإمكان التعبير عن خصائص البرمجيات — سواء كان البرنامج ينتهي، أو ما إذا كان مخرجه صحيحًا لكل مدخل — كبيانات رياضية دقيقة، فإن الأنظمة المستمدة من AxiomProver يمكنها إثباتها رسميًا، وفقًا له، مشيرًا إلى التحقق من الشيفرة التي يولدها الذكاء الاصطناعي والتي بدأت تُشغَّل في البُنى التحتية، والمالية، وأنظمة الأمن.

“العالم على وشك التشغيل على شيفرة حاسوبية لم يقرأها أحد”، قال أونو. “الذكاء الاصطناعي حاضر ولا يمكننا بعد الآن أن نتغاضى — توثيق البرهان هو منصة اختبار لحل ما أعتقد أنه أهم تحدٍ سنواجهه من الذكاء الاصطناعي”.

في الوقت الحالي، يكون ما يُسلَّم أضيق وقابلًا للفحص: خريطة من 41 مؤلفًا، مكتبة Lean عامة، وبرهان مُتحقق آليًا يُظهر أن الأعداد الأولية التي تقع ضمن 246 من بعضها لا تنفد أبدًا — أقرب جار موثق لفرضية أزواج الأعداد الأولية المتطابقة، وأعمق جزء من الرياضيات البحثية تحقق منه نظام ذكاء اصطناعي حتى الآن من البداية إلى النهاية.