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

فحصت BIG CHANGE في 7 أكتوبر قائمة ملفات المستودع كاملةً وفهرسه وبعض ملفات البراهين. وهذا تحليل توثيقي وساكن؛ لم نُجمّع مكتبة Lean أو نشغّل مدقق براهين أو نراجع الرياضيات. إعلان OpenAI يصف إصداراً متطوراً باستمرار، ويقول إن مزيداً من الصياغات الصورية سيتبع.

التغيير الكبير

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

افصلوا بين عدد المخطوطات والعائلات

وجد جردنا 722 مجلداً مباشراً للمخطوطات تحت المسار preprints/، يحتوي كل منها على ملف PDF، كما وجد 10 ملفات PDF تحت المسار reasoning_traces/. وتضم خريطة المخطوطات 372 مُدخلاً لعائلات متميزة وروابط إلى 722 مخطوطة.

تصف هذه الأعداد عناصر مختلفة:

عنصر

ما الذي يمكن للقارئ فحصه

عائلة نتائج

مجموعة من الأوراق المرتبطة، وقد تضم حججاً مكمّلة أو نتائج مترتبة أو براهين بديلة.

مخطوطة

وثيقة رياضية مستقلة لها ملفاتها المصدرية ومعلومات الاستشهاد الخاصة بها.

ملخص استدلال

عرض موجز لاستدلال النموذج بشأن نتيجة مختارة.

ملف Lean

تعريفات وعبارات وبراهين مقترحة صورية، مع روابط وإعدادات تحدد ما ينبغي فحصه.

يوضح ملف README الخاص بالمستودع هذه الفئات وينبه إلى تفاوت مستوى التحقق. فبعض النتائج لا تتضمن صياغة صورية في Lean، وتقول OpenAI إن الأعمال غير المصاغة صورياً قد تنطوي على مشكلات. ويسجل فهرس الصياغات الصورية نفسه النطاق بعبارة "تقدم جزئي" وحالة المراجعة بعبارة unchecked. وهذه الحقول بيانات وصفية للنشر، وليست نتيجة تشغيل مدقق أجرته BIG CHANGE.

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

ثبّت الإصدار قبل تتبع برهان

لقطة المستودع المستخدمة هنا هي الالتزام adc7f1241b42e322a6451854ab7e4b4c146bf78a، المؤرخ 6 أكتوبر 2026 عند 21:58:50 بالتوقيت العالمي المنسق. وتحافظ الروابط التي تتضمن هذا المعرّف على اللقطة التي فحصناها، بينما تتبع الروابط التي تتضمن main الفرع الافتراضي المتغير. ويتعهد ملف README لدى OpenAI بالاحتفاظ بالإصدارات السابقة عند ظهور تصحيحات أو مراجعات.

ابدأ بـ النظرة العامة، التي تجمع العائلات بحسب الموضوع الرياضي، ثم استخدم خريطة المخطوطات للوصول إلى ورقة بعينها. احفظ اسم مجلدها والتزام المستودع وبيانات الاستشهاد التي أرفقتها الورقة. وقد يختلف تاريخ المخطوطة عن تاريخ إصدار المجموعة العامة.

تضم العائلة 003 ورقةً تدعي وجود منطقة خالية من الأصفار إلى يمين 7/8، وبرهاناً بديلاً لمنطقة إلى يمين 11/12، وورقة مستقلة عن أصفار Landau–Siegel. ويؤرخ مجلد الورقة الأولى فيه إلى 30 سبتمبر، ويقدم استشهاداً بصيغة BibTeX. وتحديد الورقة بعينها يحافظ على التمييز بين هذه الادعاءات.

وتصف صفحة نطاق Lean العبارات التي تتناولها الصياغة الصورية، وتحدد ما تستثنيه، وتقول إن تطبيقات لاحقة في الورقة محذوفة. كما تربط بعبارات تحقق منفصلة لنتيجة دالة زيتا ودوال L من نوعي Dirichlet وHecke وفجوة موحدة للأصفار الحقيقية. ولا يمكن لفحص عبارة واحدة مختارة أن يمثل تلقائياً كل ما في تلك الصفحة.

اتبع العبارة المختارة إلى إعدادها

تستخدم تعليمات Comparator لدى OpenAI العائلة 003 مثالاً. وComparator أداة لمقارنة برهان Lean مقترح بتحدٍّ محدد. ويختار إعداد JSON في المثال نظرية واحدة: عدم انعدام دالة زيتا لريمان عندما يتجاوز الجزء الحقيقي من وسيطها 7/8.

يشير الإعداد إلى وحدة تحدٍّ ووحدة حل منفصلة. ويسمح بالمسلمات القياسية propext، Quot.sound و Classical.choice، ويضبط enable_nanoda على القيمة false. وNanoda مدقق مستقل يستطيع Comparator استخدامه؛ لكن هذا الإعداد المرفق لا يفعّله.

يحتوي ملف التحدي على sorry، وهي علامة Lean النائبة عن برهان غير مكتمل. ولها هنا وظيفة محددة: توفير العبارة المطلوب مطابقتها. وتسمح وثائق Comparator بوجود علامة نائبة في التحدي، لكنها تشترط برهاناً صحيحاً في الحل. ووجود sorry في هذا التحدي وحده لا يقول شيئاً عن اجتياز الحل المنفصل للفحص. وثائق Comparator.

في الفحص المحلي الموثق، تشمل المدخلات ذلك الإعداد ووحدتي التحدي والحل وتبعياتهما. ويثبت المستودع الإصدار Lean 4.34.1. ويسجل ملف Lake بيان مراجعات التبعيات، ومنها Mathlib عند المراجعة d13f23b723b8a846827a245b89c10fc7d3f11612.

تشترط OpenAI وجود comparator, landrun و lean4export في مسار البحث عن الملفات التنفيذية، ثم توثق تشغيل هذه الأوامر من المجلد lean/ :

Terminal
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

هذه تعليمات الناشر وليست أوامر نفذناها. وهي لا تثبت إصدارات الأدوات الخارجية الثلاث. وتشترط وثائق Comparator الحالية إصداراً متوافقاً من lean4export، وتصف متطلبات بيئة العزل والشروط التي يثبت النجاح عندها مطابقة التحدي واستخدام المسلمات المسموح بها وقبول النواة. وينبغي أن يسجل التقرير القابل لإعادة الإنتاج إصدارات الأدوات المثبتة ومخرجاتها الفعلية إلى جانب التزام المستودع.

يوصي ملف README لمكتبة Lean بتجميع أجزاء صغيرة من هذه المكتبة الكبيرة. كما يوثق حدود تعيين الذاكرة في Linux التي قد تحول دون بناء المكتبة كاملةً. ولم نقس زمن التشغيل المحلي لهذا المثال أو كلفته على الأجهزة.

اقرأ نجاح الفحص ضمن نطاقه المعلن

يفرق مرجع التحقق في Lean، بنسخته 4.35.0-rc3 عند الاطلاع عليه، بين قبول البرهان الصوري وتفسير معنى النظرية. وهذا الإصدار من الوثائق مستقل عن سلسلة الأدوات المثبتة في هذا المستودع.

يعني نجاح الفحص الأساسي أن النواة قبلت العبارة الصورية ضمن تعريفاتها ووارداتها ومسلماتها. وقد تظل في التبعيات براهين غير مكتملة. وتوثق Lean الأمر #print axioms لعرض المسلمات المستخدمة، ومنها sorryAx لبرهان غير مكتمل في سلسلة التبعيات.

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

رقم الحوسبة يصف عملية التوليد

تقول OpenAI إن كل نتيجة استخدمت في المتوسط جهداً حوسبياً يعادل نحو ثلاث ساعات من التفكير في ChatGPT Pro. ويذكر ملف README أن التقييم طرح قرابة 4,000 مسألة، ثم جمع المخرجات واختار ما عُدّ مهماً منها. كما يحدد استثناءات من الإجراء المعتاد. وهذه أرقام الشركة لعملية التوليد؛ فهي لا تسعّر فحص Lean الذي يجريه القارئ ولا تقدم فاتورة إجمالية بالدولار. إعلان الإصدار، وصف عملية التوليد.

يحدد هذا الفحص للعائلة 003 عبارةً بعينها عن دالة زيتا، والحل المقترح، والمسلمات التي يسمح بها المدقق. كما يثبت أن المثال المقدم لا يفعّل Nanoda. ولا يُعرف نجاح الفحص بهذا الإعداد إلا بتشغيل موثق.

المصادر وقراءات إضافية

  • إعلان OpenAI في 6 أكتوبريثبت تاريخ الإصدار والحالة الداخلية للنموذج والإضافات المخطط لها وتقدير الشركة للحوسبة. وهذا وصف المطور لعمله.
  • المستودع المثبتيوفر الفهرس وملفات المخطوطات وإعدادات البراهين التي فحصناها. وتستند الأعداد إلى الجرد الكامل وخريطة المخطوطات؛ أما الملفات الصورية المختارة فقُرئت من دون تشغيل. وفحصنا مصدر LaTeX للنظرة العامة لفهم تنظيمها.
  • مرجع التحقق في Leanيشرح معنى فحص البراهين وحدوده. واستخدمنا المرجع بالإصدار 4.35.0-rc3؛ بينما يثبت مشروع OpenAI الإصدار Lean 4.34.1.
  • وثائق Comparatorتشرح ملفات التحدي والحل ومتطلبات البيئة والضمانات المشروطة. وهي لا تقدم نتيجة تحقق لهذه المجموعة.
  • مراجعة Curtis Pyke على Kingy.aiتقدم فحصاً مستقلاً وساكناً للإصدار. وتصرح بعدم إجراء تشغيل مستقل لـLean؛ لذلك لا نعدّها إعادةً لفحص برهان.
  • تقرير BIG CHANGE السابق عن رياضيات الذكاء الاصطناعييغطي التسلسل من مايو إلى سبتمبر. ويفحص هذا المقال بنية ملفات المجموعة الجديدة وعملية فحصها.