وسم

| المنشور الثالث مئات المخطوطات الرياضية... من يتحقق منها؟ في المنشور الأول قلنا إن الإجابة ليست دليلًا، وفي الثاني ناقشنا حدود أدوات كشف النصوص المولدة بالذكاء الاصطناعي. اليوم ننتقل إلى ميدان يبدو أكثر حسمًا: الرياضيات. حين يعلن الذكاء الاصطناعي أنه توصّل إلى حلول لمسائل ظلت مفتوحة لعقود، • فكيف نعرف أن ما أنتجه صحيح؟ • وهل تكفي حجة تبدو مقنعة... أم نحتاج إلى وسيلة مستقلة للتحقق منها؟ لننظر في ثلاثة تطورات حديثة، وما تكشفه عن الفرق بين إنتاج البرهان والتحقق منه. 1️⃣ مئات المخطوطات... ثم تصحيح وسحب في 6 أكتوبر 2026، نشرت OpenAI مجموعة تضم 722 مخطوطة رياضية مولدة بنموذج داخلي، موزعة على 372 عائلة من النتائج. وفي اليوم التالي، سُحبت ثلاث مخطوطات بعد اكتشاف خطأ في الإشارة ضمن إحدى الحجج الرياضية، امتد أثره إلى عملين اعتمدا على البناء نفسه. كما أُجريت إصلاحات على 14 مخطوطة أخرى. أصبح العدد 719 مخطوطة، ويذكر سجل المشروع أن نحو 42% من النتائج الرئيسية لها صياغات رسمية في نظام Lean. هل يعني ذلك أن بقية النتائج خاطئة؟ لا. فغياب الصياغة الرسمية لا يثبت خطأ النتيجة، كما أن سحب بعض المخطوطات لا يبطل تلقائيًا بقية العمل. لكن الواقعة تكشف درسًا مهمًا: كثرة النتائج لا تعني أن كل نتيجة اجتازت الفحص، واكتشاف خطأ قد يستلزم مراجعة الأعمال التي تعتمد عليه. المصدر الأصلي: github.com/openai/math/blob/mai… 2️⃣ من الحجة المكتوبة إلى البرهان القابل للتحقق الرسمي في 15 أكتوبر 2026، أعلن مختبر شنغهاي للذكاء الاصطناعي عن عمل تعاوني بين باحثين ونموذج Intern-S2 أسهم في إثبات حالة من حدسية Ghys في الهندسة الديناميكية. تثبت الورقة حدسية Ghys في حالة الرتبة المشتركة الواحدة، المعروفة باسم codimension-one، وتشمل الحالة ثلاثية الأبعاد في الفضاء المركب. ولم يتوقف العمل عند كتابة البرهان؛ فقد صاغ فريق من جامعة بكين المبرهنات الرئيسية في نظام Lean للتحقق الرياضي الرسمي، باستخدام إطار SHEAF. وبحسب إعلان الفريق، استغرق العمل نحو خمسة أيام، وبلغ حجم الشيفرة قرابة 550 ألف سطر، مع تشغيل ما يصل إلى 100 وكيل بالتوازي. لكن الدقة تقتضي توضيح أمرين: أولًا: لا تعني النتيجة حل حدسية Ghys في جميع الحالات؛ فالورقة تثبتها في حالة الرتبة المشتركة الواحدة، بينما تبقى الحالات ذات الرتب المشتركة الأعلى مفتوحة عمومًا. ثانيًا: يوضح البحث أن المؤلف استخدم نموذج Intern-S2 للمساعدة في تطوير الأفكار والحجج الرياضية، وأنه تحمّل المسؤولية عن التحقق المستقل من الحجج. كما صيغت النتائج المركزية رسميًا في Lean، مع تحقق بشري من المبرهنة النهائية. إذن نحن أمام تعاون بين الإنسان والذكاء الاصطناعي، تدعمه أدوات للتحقق الرسمي، لا أمام إنجاز مستقل للنموذج وحده. المصادر الأصلية: إعلان مختبر شنغهاي: shlab.org.cn/news/5444307 الورقة البحثية: arxiv.org/abs/2609.37695 الشيفرة الرسمية: github.com/frenzymath/Holomorph… 3️⃣ مسائل رياضية مفتوحة... هل تستطيع الآلة حلها؟ في بحث بعنوان «Advancing Mathematics Research with AI-Driven Formal Proof Search»، درس باحثون قدرة أنظمة الذكاء الاصطناعي على البحث عن براهين رسمية لمسائل رياضية مفتوحة. وبحسب ملخص البحث، حقق النظام الأقوى في الاختبارات النتائج الآتية: • حل 9 مسائل من أصل 353 مسألة مفتوحة من مسائل إردوش جرى اختبارها. • أثبت 44 حدسية من أصل 492 حدسية ضمن مجموعة اختبارات مستمدة من موسوعة المتتاليات الصحيحة على الإنترنت OEIS. هذه مجموعتان منفصلتان من الاختبارات، وليستا مقياسًا عامًا لقدرة النظام على حل جميع المسائل الرياضية المفتوحة. وتكمن أهمية هذا النهج في استخدام Lean للتحقق من البراهين الرسمية، بدل الاكتفاء بحجج مكتوبة بلغة طبيعية قد تبدو مقنعة رغم احتوائها على أخطاء. ومع ذلك، يظل من الضروري التأكد من أن الصياغة الرسمية تمثل المسألة الأصلية بدقة، وأن النتيجة لا تتجاوز ما تسمح به افتراضاتها. المصادر: البحث العلمي: arxiv.org/abs/2605.22763 مستودع النتائج: github.com/google-deepmind/alph… 🔬 ما الفرق بين إنتاج البرهان والتحقق منه؟ لفهم هذه التطورات، ينبغي التمييز بين ثلاثة مستويات: إنتاج البرهان: أن يقترح النظام حجة أو مسارًا لحل مسألة رياضية. التحقق الرسمي: أن تُصاغ الحجة بلغة رياضية دقيقة يستطيع نظام مثل Lean فحص خطواتها وفق قواعده وافتراضاته. المراجعة العلمية: أن يفحص المختصون معنى النتيجة، وصحة صياغة المسألة، والافتراضات المستخدمة، ومدى جدة النتيجة وأهميتها. هذه المستويات يكمل بعضها بعضًا، لكنها ليست شيئًا واحدًا. فالتحقق الرسمي يقدم ضمانًا قويًا بشأن صحة البرهان المرمّز ضمن النظام وافتراضاته، لكنه لا يثبت وحده أن الصياغة المرمّزة تطابق المسألة المقصودة تمامًا، ولا يحسم أهمية النتيجة العلمية. وفي المقابل، ليس كل برهان رياضي غير مكتوب بلغة رسمية برهانًا خاطئًا؛ فالبراهين التقليدية يمكن أن تكون صحيحة ومقبولة بعد الفحص والمراجعة العلمية. الخلاصة يفتح الذكاء الاصطناعي آفاقًا مهمة أمام البحث الرياضي، من اقتراح أفكار جديدة إلى استكشاف مسارات قد يصعب على الباحثين اختبارها يدويًا. لكن لا ينبغي أن نخلط بين كثرة النتائج وصحتها، ولا بين الحجة المقنعة والبرهان الذي اجتاز الفحص. قيمة الإنجاز ليست في أن تنتج الآلة برهانًا فحسب، بل في أن يصبح قابلًا للفحص والنقد وإعادة التحقق. وهذا هو جوهر منهجنا في «الذكاء الاصطناعي تحت المجهر»: 🔬 نتحقق أولًا، ونحلل ثانيًا، ثم نكتب للنشر. #غواص_المعاني أغوص في بحر القراءة... لأعود بدرة.💎 #الذكاء_الاصطناعي_تحت_المجهر #الذكاء_الاصطناعي #الذكاء_الاصطناعي_إلى_أين؟ #الرياضيات #البحث_العلمي