OpenAI تضيف إلى مستودعها الرياضي ورقة تدّعي أن فرضية Exponential Time Hypothesis خاطئة
المغزى: ما يحدد قيمة مخرجات النموذج هو أدوات التحقق المبنية حوله، فحين أثبت Lean حدًّا أضعف من دعوى الورقة، انتقل الحكم الأخير إلى مراجعين من البشر.
مقالة ضيف على مدونة Terence Tao: إثباتات النماذج الطويلة قد تجعل المعرفة غريبة عن الفهم البشري
المغزى: الخطر الذي تصفه المقالة ليس إثباتًا خاطئًا، بل إثبات صحيح لا يستطيع إنسان قراءته، وطريق إلى المعرفة تملكه شركات قليلة حتى دون سوء نية من أحد.
خطأ في إشارة رياضية يُسقط ثلاث أوراق من مستودع OpenAI للرياضيات
المغزى: العيب في نتيجة واحدة ينتقل إلى كل ما بُني عليها، تمامًا كما ينتقل عيب حزمة برمجية إلى كل مشروع يستوردها، وأغلب ما في المستودع لم تفحصه آلة بعد.
OpenAI تنشر 722 ورقة رياضيات من نموذج داخلي، و162 منها فقط ببرهان يتحقق منه الحاسوب
المغزى: الرقم المهم ليس عدد الأوراق بل نسبة ما تحقق منه الحاسوب، نحو 22%، والباقي يظل دعوى تنتظر مراجعة بشرية باعتراف الشركة نفسها.
برهان رياضي كبير بمساعدة Claude وCodex يُتحقق منه في Lean، ومؤلفاه يصفان مسودته الأولى بأسوأ كتابة
المخرج الضخم الذي يصعب على البشر قراءته يصبح مقبولًا حين تقف خلفه أداة آلية تحكم بالصحة أو الخطأ، وهو الدور نفسه الذي تؤديه الـ tests للكود الذي تكتبه الوكلاء.
Anthropic تصيغ برهان مبرهنة فيرما الأخيرة بلغة Lean في 11 يومًا
حين يوجد حَكَم آلي يرفض الخطأ، يستطيع الـ agent العمل أيامًا وإخراج نتيجة صحيحة. وما لا يملك حكمًا كهذا، وهو أغلب البرمجيات، ما زال يحتاج مراجعة بشرية.
OpenAI تعلن عن نموذج Astra بعد نتائج في 10 مسائل رياضية مفتوحة
ما يجعل الادعاء قابلًا للتصديق ليس النموذج بل Lean: نظام يتحقق آليًا من كل خطوة في البرهان، فلا تمر الهلوسة مهما كانت مقنعة.