722 برهانًا من ذكاء اصطناعي: ما الذي يمكن التحقق منه الآن

في ليلة السادس إلى السابع من أكتوبر، بعد منتصف الليل بتوقيت إسبانيا، رفعت OpenAI إلى GitHub 722 مخطوطة رياضية. كتبها نموذج داخلي لم تطلقه الشركة ولم تكشف اسمه، وهي موزعة على 372 «عائلة»: تجمع كل عائلة نتيجة رئيسية مع صيغها المختلفة ونتائجها المترتبة عليها. وتوضح OpenAI أنها تقيّم نماذجها بمسائل بحثية لم تُحلّ بعد، وأنها نشرت النتائج التي بلغت مستوى كافيًا من الأهمية.

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

كتب لانس فورتنو (Lance Fortnow)، أحد قدامى الباحثين في نظرية الحوسبة، في اليوم التالي أن مجاله تقدّم في 24 ساعة أكثر مما تقدّم في العقود الثلاثة السابقة مجتمعة. وأضاف في التدوينة نفسها أن شيئًا من ذلك لم يُتحقَّق منه بعد.

هذا التحفظ هو سؤال هذا المقال: ماذا يعني أن تكون هذه النتائج «مُتحقَّقًا منها». هذه المرة يمكن لآلة أن تراجع جزءًا منها، وهو أمر لم يحدث مع أي إعلان سابق. لكن لهذه المراجعة طبقات، ومعظم العمل لم يُنجَز بعد.

ما الذي يحتويه المستودع بالضبط

وفقًا لـملف README في المستودع، تلقّى النموذج نحو 4000 مسألة، واستهلكت كل نتيجة في المتوسط قدرًا من الحوسبة يعادل ثلاث ساعات من استدلال ChatGPT Pro. لا تشرح الشركة كيف اختارت تلك المسائل، لكنها تكشف نسبة: من نحو 4000 محاولة خرجت 372 عائلة. وكما يشير فورتنو، حلّ النموذج أقل من 10% مما طُرح عليه.

جرى الحصول على كل شيء تقريبًا بالإجراء الآلي نفسه. ويعترف ملف README باستثناءين دون تفصيلهما: منطقة من دالة زيتا لريمان لا توجد فيها أصفار، وحدسية هودج لعائلة معينة من الكائنات الهندسية. وهما تحديدًا النتيجتان الأقرب إلى مسائل الألفية. كما أن أحد النصوص المتعلقة بدالة زيتا حرّره بشر ليصبح مقروءًا.

يتضمن المستودع:

• المقالات بصيغة PDF مع ملفاتها المصدرية؛
• عشرة ملخصات مختصرة للاستدلال الذي اتبعه النموذج؛
• مكتبة من البراهين الرسمية في Lean، سنتحدث عنها بعد قليل؛
• والتزامًا بالحفاظ على السجل: ستُنشر التصحيحات في إصدارات جديدة، دون حذف الإصدارات السابقة.

ويحذّر ملف README نفسه: «Some of the unformalized results could have issues». أي أن بعض النتائج التي لم تُصَغ صياغة رسمية قد تكون فيها مشكلات.

منشور الإعلان لا يُبرز أي نتيجة بعينها. وقائمة «النتائج الكبرى» المتداولة هذه الأيام اختيارٌ من الصحافة ومن الرياضيين أنفسهم. وقد اخترنا أربعًا منها تساعد على فهم حجم ما يُدَّعى.

أربع نتائج لفهم ما هو على المحك

الأعداد الأولية ودالة زيتا

تبدو الأعداد الأولية موزعة بلا نظام، لكنها تتبع قانونًا متوسطًا بُرهن عليه عام 1896: حتى العدد x يوجد تقريبًا x/ln x عددًا أوليًا. والسؤال المثير هو مقدار ابتعاد العدد الفعلي عن هذا القانون. وتتوقف الإجابة على مواضع أصفار دالة زيتا لريمان، أي النقاط التي تساوي فيها هذه الدالة صفرًا.

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

تقول OpenAI إنها برهنت عليها: لا توجد أصفار جزؤها الحقيقي أكبر من 7/8. ليست هذه فرضية ريمان، التي تتطلب الوصول إلى 1/2، لكنها ستكون أول تقدم من هذا النوع منذ طرح السؤال. وتستبعد مخطوطة أخرى من العائلة نفسها كذلك ما يُسمّى أصفار سيغل، وهي شذوذ افتراضي يجعل كثيرًا من المبرهنات حول الأعداد الأولية تعتمد على ثوابت لا يعرف أحد كيف يحسبها. وتبرهن مخطوطة ثانية، بطريق آخر، على منطقة أصغر قليلًا تبدأ من 11/12. وهي النص الذي حرّره بشر.

حدود خوارزميات التحسين

كثير من المسائل العملية أصعب من أن تُحلّ حلًّا دقيقًا على نطاق واسع. ومن أمثلتها تقسيم شبكة إلى مجموعتين بحيث يُقطع أكبر عدد ممكن من الروابط (Max-Cut). ومثال آخر هو اختيار أقل عدد من العُقد يلامس جميع الروابط (Vertex Cover). في هذه الحالات نستخدم خوارزميات تعطي إجابة تقريبية بجودة مضمونة. فخوارزمية Max-Cut مثلًا تضمن 87.8% على الأقل من الحل الأمثل.

منذ 2002، تتنبأ حدسية الألعاب الفريدة (Unique Games)، التي صاغها سوبهاش خوت (Subhash Khot)، بأنه لا يمكن تحقيق ما هو أفضل في وقت معقول. وإذا صحّت، فإن كثيرًا من الخوارزميات التقريبية التي نستخدمها بالفعل ستكون أفضل ما يمكن، ما لم يكن P = NP. وتقول OpenAI إنها برهنت على الحدسية. وفي نتيجة منفصلة، تقول كذلك إنها تثبت، دون الاعتماد عليها، أن تحسين تلك الضمانات لـMax-Cut وVertex Cover مسألة NP-صعبة، أي إنها بصعوبة أصعب المسائل في فئتها.

وهنا قصة إنسانية. وفقًا لـQuanta Magazine، بدأت في 11 سبتمبر شائعات بأن OpenAI تملك البرهان. وكان دور مينزر (Dor Minzer) من MIT وطالبان يعملون منذ سبع سنوات على صيغة من المسألة، وقد حلّوها في أبريل. وبعد ثلاثة أيام من الشائعات نشروا 95 صفحة مع تنبيه في الصفحة الأولى: النص مكتمل رياضيًا، لكنه ليس بالشكل الذي أرادوا أن يشاركوه به. وقال مينزر للمجلة: «There is a lot of value in failing and knowing why you failed»، أي أن للفشل ولفهم سببه قيمة كبيرة.

لماذا يبقى المغناطيس مغناطيسًا

في المغناطيس تصطفّ العزوم المغناطيسية الصغيرة للذرات، أي السبينات. وتصف الفيزياء الكمومية هذا السلوك بنموذج هايزنبرغ، وكل فيزيائي يسلّم بأن المادة في ثلاثة أبعاد، وعند درجة حرارة منخفضة، تحتفظ بمغنطتها. لكن البرهان على ذلك بصرامة أمر آخر. فقد حُلّت منذ عقود الصيغة الكلاسيكية من النموذج والحالة الكمومية ضديدة المغناطيسية، التي تشير فيها السبينات المتجاورة إلى اتجاهين متعاكسين. لكن التقنية التي نجحت في تلك الحالات لا تصلح للمغناطيس الكمومي العادي، وقد أدرجه إليوت ليب (Elliott Lieb) عام 1999 بوصفه «Problem A» في قائمة من المسائل المفتوحة في الفيزياء الرياضية.

تقول OpenAI إنها برهنت عليه في جميع الأبعاد ابتداءً من ثلاثة. وهو مثال جيد على نوع من النتائج يمرّ عادةً دون أن يلفت الانتباه: لا يغيّر ما نعتقده عن العالم، لكنه يحوّل يقينًا فيزيائيًا إلى مبرهنة.

سؤال كلاسيكي بإجابة غير متوقعة

انطلاقًا من «زمرة حرّة»، أي مجموعة كل الكلمات التي يمكن كتابتها بحرفين ومعكوسَيهما، أو بثلاثة أحرف، يُبنى كائن من التحليل يُسمّى عامل فون نويمان. تظهر هذه الكائنات في الأعمال التأسيسية لموراي وفون نويمان، والسؤال، الذي يُنسب إلى ريتشارد كاديسون (Richard Kadison)، هو: هل يتذكر الكائن عدد الأحرف التي بدأنا بها؟ تُعدّ هذه أشهر مسألة مفتوحة في مجالها، وقد اتجه جزء كبير من البحث إلى البرهان على أن هذه الكائنات مختلفة.

تقول OpenAI العكس: بحرفين أو بثلاثة نحصل على الكائن نفسه. وإذا تأكد ذلك، فستكون من تلك النتائج التي تفرض مراجعة حدس مجال بأكمله. كما أنها توضح جيدًا المشكلة التي يتناولها القسم التالي.

بقية الفهرس

هذه النتائج الأربع مجرد عيّنة. يجمع الجدول نتائج أخرى من الصف الأول، ويبيّن هل لها برهان رسمي في Lean:

المصدر: فهرس المستودع وفهرس الصياغات الرسمية، جرى الاطلاع عليهما في 7 أكتوبر 2026. أوصاف مبسّطة من إعداد Codin.

«مُتحقَّق منه» قد يعني ثلاثة أشياء مختلفة

الجديد في هذا النشر مقارنةً بما سبقه هو Lean. وLean لغة يُكتب فيها البرهان بتفصيل يكفي لأن يراجعه برنامج خطوة خطوة، دون أن يثق بأحد. وتعتمد على Mathlib، وهي مكتبة مجتمعية من التعريفات والمبرهنات التي سبق التحقق منها. وحين «يُصرَّف» البرهان في Lean (compile)، فهذا يعني أن كل خطوة تنتج عمّا سبقها.

لكن حين يقال إن نتيجة ما مُتحقَّق منها، يجدر التمييز بين ثلاثة أسئلة.

الأول: هل البرهان الرسمي صحيح؟

هذا ما يحسمه Lean، ويمكن تكراره خارج OpenAI. يتضمن المستودع تحديات لأداة Comparator، وهي أداة لا تقبل البرهان إلا إذا أثبت المنطوق المرجعي بالضبط ولم يستخدم إلا البديهيات المعيارية. وبعد ساعات قليلة من النشر، أعاد عدة أشخاص من خارج OpenAI تصريف برهان منطقة 7/8 على أجهزتهم، وكانت النتيجة صحيحة.

يحتوي المستودع على أكثر من 120 ألف ملف Lean، لكن هذه المكتبة لا تغطي إلا جزءًا صغيرًا من الفهرس: 162 من أصل 722 مخطوطة صيغت نتيجتها الرئيسية صياغة رسمية.

الثاني: هل يقول المنطوق الرسمي ما نظنه؟

يضمن Lean أن البرهان يثبت المنطوق الذي أُعطي له. ولا يضمن أن هذا المنطوق يعني ما يقوله المقال. وهذه الطبقة هي الأكثر اعتمادًا على البشر، وتتفاوت صعوبتها كثيرًا من نتيجة إلى أخرى.

في أفضل الحالات، يكون المنطوق قصيرًا إلى حدّ أن أي شخص لديه قدر من التكوين يستطيع قراءته:

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
  sorry

إذا كان التعريف هو تعريف المجتمع وكان المنطوق يتسع في سطرين، فإن الثقة التي يمنحها Lean عالية جدًا. ولهذا فإن منطقة 7/8 الخالية من الأصفار هي اليوم أفضل نتيجة مُتحقَّق منها في الفهرس.

حالة عوامل الزمر الحرة مختلفة. فـMathlib لا تتضمن هذه الكائنات بعد، ولذلك يعرّفها تحدي Comparator من الصفر، بتعريفات كتبتها OpenAI أيضًا. ويحدث شيء مشابه مع Unique Games: يستند المنطوق إلى آلاف المحارف من الترميزات الخاصة. والبرهان المثالي لتعريف خاطئ قليلًا يبرهن على شيء آخر. لا بد أن يقرأ هذه التعريفات شخص ملمّ بالمجال ويؤكد أنها تعبّر عن المسألة الحقيقية.

ويوضح فهرس الصياغات الرسمية ذلك في حقلين: براهين Lean كتبها أيضًا وكيل ذكاء اصطناعي (automation: agent)، ومراجعتها مسجّلة على أنها معلّقة (review: unchecked).

الثالث: ماذا فهمنا؟

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

أما المخطوطات الـ560 الأخرى فتعتمد اليوم على نصها باللغة الطبيعية وعلى التقدير الداخلي لـOpenAI. ومن بينها حدسية هودج، إحدى النتيجتين اللتين لم تتبعا الإجراء الآلي، وليست لها صياغة رسمية.

ثم يبقى ما لا يراجعه أي برنامج: ما الفكرة التي تجعل كل برهان يعمل، وهل يفتح طرقًا جديدة، وما الذي يتغير في المجال. تحدثنا عن هذا التحول في حين يتوقف البرهان عن أن يكون عنق الزجاجة. وهذا النشر يجعله ملموسًا: لقد جعلت الآلة الطبقة الأولى أسهل بكثير، ويتركز العمل البشري في الطبقتين الأخريين.

ما طلبه الرياضيون وما وصل

في 21 سبتمبر، قدّمت OpenAI مجموعة استشارية مستقلة من تسعة رياضيين، هي AGMAI، مقرها معهد الدراسات المتقدمة في برينستون. وفي 29 سبتمبر، قبل أسبوع من النشر، نشرت المجموعة توصياتها، المبنية على أكثر من 600 ردّ من المجتمع الرياضي. وبدأت بطلب: أن تتوقف المختبرات عن اختبار المسائل الرياضية المتقدمة على نماذج مملوكة لها. وهذه مقارنة بين ما طُلب وما وصل:

المصادر: توصيات AGMAI بتاريخ 29 سبتمبر، وإعلان OpenAI، وملف README في المستودع. المقارنة من إعداد Codin.

من دون النموذج والموجّهات، لا يستطيع أحد إعادة إنتاج الطريقة التي وُصل بها إلى كل نتيجة. وهذا لا يمنع التحقق من برهان، فالبرهان يصمد أو لا يصمد بذاته. لكنه يمنع معرفة وزن اختيار المسائل، وما جُرّب دون نجاح، وهل تلقّى الاستثناءان مساعدة لم تتلقها البقية.

وفي اليوم نفسه، 6 أكتوبر، نشرت AGMAI بيانًا يستحق أن يُقرأ كاملًا. يقول إن دورها الاستشاري لا ينبغي أن يُفهم على أنه تقييم لأثر هذه النتائج ولا تزكية للعملية. ويضيف أن الحكم على مدى اتباع توصياتها شأن المجتمع الرياضي. ويلخّص ذلك هكذا: «This release is the beginning, not the completion, of the process». أي أن النشر هو بداية عملية فهم هذه النتائج واستيعابها، لا نهايتها.

كيف استقبلها المجتمع الرياضي في الساعات الأولى

حتى 7 أكتوبر، لم يكن أي متخصص قد نشر مراجعة لنتيجة بعينها، ولم يُؤكَّد أي خطأ. الموجود حتى الآن مواقف من طريقة قراءة الإعلان.

طالب أندرو ساذرلاند (Andrew Sutherland) من MIT، في Scientific American، بمعاملة ما لا يمكن إعادة إنتاجه على أنه غير مُتحقَّق منه: «We should ask for receipts»، أي علينا أن نطلب ما يثبت ذلك. وردّ دانيال ليت (Daniel Litt) من جامعة تورونتو في المقال نفسه بالحجة المعاكسة. فإذا أردنا معرفة الإجابات، فلا معنى لمطالبة الشركة بإبقائها سرًّا، وهو يرى أن ذلك سيكون في صالح الرياضيات. وقال مارك برافرمان (Mark Braverman) من برينستون لـQuanta إن الرياضيات عبر البيانات الصحفية «ليست صحية جدًا»، مع أنه أقرّ بأن برهانًا كهذا قد يفتح مسارات جديدة.

في الأثناء، بدأ التحقق ينتظم خارج OpenAI. فإلى جانب إعادة تصريف براهين Lean، استورد فهرس مجتمعي للمسائل المفتوحة مئات النتائج، مع التحذير نفسه على كل واحدة منها: لم يراجعها أي رياضي مستقل بعد. وهو يصنّف عدة نتائج بالفعل على أنها موضع خلاف، بسبب تعارض محتمل مع نتائج منشورة من قبل.

للنبرة العامة وجهان. هناك دهشة من الحجم، حتى بين المنتقدين. وهناك إرهاق: فبعد الجدل حول نسبة برهان نافييه–ستوكس ورسالة الحائزين على ميدالية فيلدز، لم يعد النقد موجّهًا إلى ما تقوله هذه الأنظمة فحسب، بل أصبح موجّهًا أيضًا إلى من يقرر الإيقاع وإلى طريقة النشر.

الاختبار الناجح لا يثبت إلا ما يسأل عنه

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

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

لذلك، الرقم الذي يجدر متابعته في الأشهر المقبلة ليس 722. هناك ثلاثة أرقام أخرى ستقول أكثر:

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

إذا ارتفعت هذه الأرقام، فسيكون هذا النشر قد ساعد المجتمع الرياضي على استيعاب نتائج حقيقية. وإن لم ترتفع، فسيكون لدينا مئات المبرهنات التي لا نعرف عنها إلا أن آلة تقول إنها صحيحة.

المصادر

• OpenAI: «Sharing AI progress in mathematics»، 6 أكتوبر 2026.
• مستودع openai/math: README، وفهرس المخطوطات، وفهرس الصياغات الرسمية، ونطاق الصياغة الرسمية لفرضية شبه ريمان، وتحدي Comparator. الإيداع (commit) adc7f124، جرى الاطلاع عليه في 7 أكتوبر 2026.
• AGMAI: توصيات 29 سبتمبر 2026 وبيان 6 أكتوبر.
• لانس فورتنو: «Open No More»، 7 أكتوبر 2026.
• Quanta Magazine: السباق نحو حدسية الألعاب الفريدة، 7 أكتوبر 2026.
• Scientific American: ردود ساذرلاند وليت، 6 أكتوبر 2026.
• إليوت ليب: «Problem A»، قائمة المسائل المفتوحة في الفيزياء الرياضية، 1999.
• عمليات إعادة تصريف مستقلة لبرهان منطقة 7/8: Zhang-Liao/quasi-riemann وdavegoldblatt/openai-zeta-proof-check. وهي تتحقق من البرهان الرسمي، لا من المقال.
• الفهرس المجتمعي vibemathed: استيراد نتائج OpenAI.

ملاحظة تحريرية: لم ندقق أيًّا من النتائج. الأوصاف الرياضية مبسّطة لقارئ غير متخصص، وتعكس ما تدّعيه OpenAI، لا إجماعًا في المجتمع الرياضي.