أحدث نموذج استدلال داخلي من OpenAI، أطلق عشرة تقدمات رائعة في الرياضيات دفعة واحدة.
وتشمل:
- تم إثبات وجود مجموعات غير سوفيك (Non-sofic groups) لأول مرة؛
- تم تقديم حدود دوائر جديدة تمامًا (Circuit lower bounds)؛
- تم حل حد صعوبة مشكلة المتجه الأقرب (Closest Vector Problem، CVP)؛
- وأيضًا نظرية التكرار المتوازي الكمومي للعبة ثنائية مع انخفاض أسّي.
ما يهتم به الأستاذ المساعد في جامعة كولومبيا هنري يوان هو الأخير—
في عام 2016، حقق يوان تقدمًا كبيرًا في هذه المسألة، لكنه لم يحلها تمامًا. على مدار عشر سنوات، فشل مرارًا وتكرارًا، وحتى قبل شهر، حاول مرة أخرى باستخدام ChatGPT 5.5 للوصول إلى الإثبات النهائي، لكنه حصل على نتائج ضئيلة.
وكان الذكاء الاصطناعي على كتفه، فدفع الكرة بلطف داخل المرمى.
أثبتت الصواب، لكن البشر لم يفهموا
قبل بضعة أيام، أرسل لي جي تشين مسودة ورقة بحثية إلى هنري يوان وآخرين.
كانت الحياة مشغولة آنذاك، فلم يكن لديه وقت لدراسة الأمر بعمق. الآن، تم نشر الورقة البحثية. إنه يشعر بأنه مضطر للتحدث، لديه ما يقوله.
نظرية التكرار المتوازي الكمي (Quantum parallel repetition theorem)، هي المجال الذي قضى هنري يوان سنوات عديدة في دراسته أثناء دراسته الجامعية، وهي أكثر إنجازاته فخرًا.
هنري يوان، أستاذ مشارك في علوم الحاسوب في عائلة سريفاني بجامعة كولومبيا
لقد تذكر تلك الظهائر التي قضاها في المقاهي، والليالي المتأخرة التي قضاها في المكتب، والعديد من عطلات نهاية الأسبوع التي كان ينبغي أن يرتاح فيها، وهو يعيد تحليل ودراسة نظرية ران راز المتكررة المتوازية مرارًا وتكرارًا.
كان يرغب في حل النسخة الكمية من هذا المبرهنة، لدرجة أنه لم يستطع النوم وظل يقلّب في فراشه. لقد استهلك كميات هائلة من الأدوات الرياضية، ونجح أخيرًا في إثبات التناقص كثير الحدود.
https://arxiv.org/pdf/1604.04340
الأهم من ذلك، أنه بنى ثقةً من خلال ذلك، وأدرك أخيرًا قدراته، وأثبت أنه قادر بالفعل على حل تلك المشكلات (على الأقل جزء منها) التي يهتم بها الآخرون أيضًا.
هو يؤمن أن إثبات OpenAI هذا يجب أن يكون صحيحًا، نظرًا لوجود إثبات مُصاغ بـ Lean. لكن هنري يوان لا يزال بحاجة إلى بعض الوقت لفهم هذا الإثبات الجديد.
على الرغم من أن الإثبات الجديد يواصل من حيث انتهى السابق، إلا أن الذكاء الاصطناعي تجاوز قيود استراتيجية الإثبات الأصلية، مستخدمًا بعض الحيل والأساليب التي ربما كانت معروفة بالفعل للباحثين في مجالات نظرية المشغلين والتحليل الوظيفي.
بخلاف الإثارة، كان الشعور الأول ليوين هو الإحباط، إحباطًا من أسلوب كتابة البحث.
قال إن هذا الإثبات يقرأ وكأنه مكتوب بالذكاء الاصطناعي: مقدمة طويلة ومطولة تدور حول نفسها، بينما الأجزاء الأساسية تبدو كسحر، مما يُربك القارئ.
إثبات OpenAI، الذي يُقرأ باهتمام كبير، لكنه أيضًا مُربك بعض الشيء.
إنها تضع المشكلة بشكل منظم على الطاولة أولاً، ثم تقفز فجأة إلى اتجاه "استخدام التحليل المسبق للعثور على التصفية الصحيحة"، دون ترك أي خطوات منطقية تقريبًا في الوسط.
بعد ذلك، تأتي سلسلة من حسابات إنتروبيا المصفوفة الغريبة، والتي تُجرى بتعقيد حتى تُخبرك: أن هذا الطريق ممكن.
لكن الخطوة الأهم، تلك الحدس، من أين جاء، لم تذكر.
أما أدق وأكثر اللحظات إبداعًا وتحديًا — وهي تقنية توسيع فضاء المشغل باستخدام تحويل أولمان (Uhlmann transformation) — فكان ينبغي أن تكون ذروة الإثارة في الإثبات بأكمله، لكن الذكاء الاصطناعي تخلّى عنها كأنها رمل وحصى، وطرحها في القسم الرابع دون أي تحذير أو تفسير.
الإثبات الصحيح، لكن الفكرة الأهم مخفية.
He hopes OpenAI will spend a few more prompts to properly organize this manuscript.
الأكثر إيلامًا هو الطبقة الثانية: التحقق من Lean لا يعني الفهم.
يمكن للآلة ضمان أن كل خطوة استدلالية لا تشوبها شائبة، لكنها لا تستطيع الإجابة عن الأسئلة مثل: "لماذا تعمل هذه الطريقة؟" أو "ماذا تعني في السياق النظري الأوسع؟" أو "أين يمكن استخدامها؟" — Lean لا يستطيع الإجابة عن أي من هذه الأسئلة.
يُعترف يوان بأنه لا يزال يتعامل مع هذا الدليل حتى الآن.
الإجابة أمامه، لكنه يرغب في إعادة بناء الحدس الذي لم يُصرّح به الذكاء الاصطناعي، سطرًا سطرًا، كما لو كان يقرأ ورقة بحثية لغير المتخصصين.
نعم، هناك دليل Lean هناك. لكنه مجرد تشكيل رسمي، ولا يعني أنني فهمت. لفهمه حقًا، ربما لا يبقى سوى الانتظار والتمرين بمرور الوقت.
بالفعل، وسّع الذكاء الاصطناعي حدود فهم البشر، لكن ثم ماذا؟ ماذا يبقى من متعة البحث ومعناه؟ إذا حلّ الذكاء الاصطناعي جميع المشكلات التي كان يشغل باله، فماذا يبقى له؟
تتالت الأسئلة. لكن هناك نقطة أصبحت أكثر وضوحاً لديه: لن يكون لدى الرياضي وقت فراغ في الأيام القادمة، فعليه ترويض هذه الوحوش الفكرية وترجمة لغتها التقنية إلى لغة مفهومة.
تم كشف زيف ادعاء أن الذكاء الاصطناعي "أثبت خطأ" فرضية رياضية قديمة منذ مائة عام! Lean ليس خزنة آمنة
في الأسبوع الماضي، نفى رامانا كومار فرضية كولاتز الشهيرة، أشهر معضلة رياضية غير محلولة، باستخدام 300 سطر من Lean.
السؤال الذي طرحته بسيط جدًا: لديك عدد صحيح موجب، وتنفذ عمليتين متكررتين وفقًا لقاعدتين — إذا كان زوجيًا، اقسمه على 2؛ إذا كان فرديًا، اضربه في 3 وأضف 1 — فهل سينتهي الأمر دائمًا بالوصول إلى 1، بغض النظر عن الرقم الذي تبدأ به؟
يمكنك حساب:
هذه الفرضية تقول إنه بغض النظر عن أي عدد صحيح موجب تبدأ به، فستنتهي دائمًا في هذه الدورة 4→2→1.
لم يتمكن أحد من إثبات صحته أو إيجاد مثال مضاد منذ أن طرحه الرياضي لوثار كولاتز عام 1937.
وصفه الرياضي بول إيردوس بأنه: "الرياضيات غير مستعدة لمواجهة مثل هذه المشكلة"، واعتبر جيفري لاغارياس، عضو الأكاديمية الوطنية الأمريكية للعلوم والرياضيات، أن "هذه مشكلة صعبة بشكل استثنائي، وخارجة تمامًا عن نطاق الرياضيات المعاصرة".
If falsified, it would undoubtedly be a groundbreaking news in the mathematical community.
للأسف، بعد ثلاثة أيام، تم إبطال الإثبات الرسمي لـ Lean لأنه استغل في الواقع ثغرة أساسية في نواة Lean.
دينيال سيلسام من OpenAI، بمساعدة ذكاء اصطناعي متخصص في أمن الشبكات، قام بإجراء مراجعة للنواة مع Lean FRO.
كما اكتشفوا أكثر من ثغرة واحدة داخل نواة Lean!
في نفس الوقت تقريبًا، نشر ألكس كونتوروفيتش، أستاذ الرياضيات في جامعة روتجرز ومستشار منظمة Lean البحثية، منشورًا يحذر من عدم اعتبار Lean مُحققًا شاملاً.
لقد أشار مباشرة إلى النقطة الضعيفة — التزامن الدلالي (Semantic Alignment).
حتى لو كان نواة Lean خالية من العيوب، فإن Lean تهتم فقط بترجمة الكود. من يضمن أن "التعريفات" التي تكتبها في الكود هي نفسها "النية البديهية" التي يفهمها البشر باللغة الطبيعية؟
ما يمكن لـ Lean التأكد منه هو شيء واحد فقط: أن الكود يُركّب بنجاح، وأن المنطق الشكلي صحيح. لكنه لا يتحقق أبدًا من مشكلة أكثر خطورة: هل هذه العبارة المُشكّلة تتوافق حقًا مع النظرية التي ترغب في إثباتها؟
تم إثبات المبرهنة بشكل صحيح، لكن السؤال نُسخ خطأً، وظل Lean يعطي الإشارة الخضراء.
لكن هذه المشكلة في المحاذاة لا يمكن حلها بالكامل باستخدام الحاسوب.
في محاضرة ICM 2026، أشار كونتوروخيف إلى أن أكبر نقطة عمياء في الرياضيات التشكيلية ليست في "الاشتقاق الصحيح"، بل في "القول الصحيح". في النهاية، يجب أن يكون الخبراء البشريون هم من يتحققون من النتائج.
كان السبب الذي جعل تجربة السائل التحليلي تُعتبر أسطورية هو المراجعة اليدوية الدقيقة شبه المهووسة من قبل الباحثين لكل تعريف رياضي.
عند النظر إلى كلمات الأستاذين معًا، فإنها تشير إلى نفس الحقيقة: يمكن للذكاء الاصطناعي إثبات ذلك، ويمكن للآلات التحقق منه، لكن الفهم والرقابة لا يزالان من مهام الإنسان.
أخيرًا، هناك شائعة حول نموذج استدلال الذكاء الاصطناعي:
المراجع:
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
هذا المقال من حساب WeChat "New Intelligence Yuan"، المؤلف: Revelation of ASI؛ التحرير: ديفيد