تحوّلت مسائل عالم الرياضيات المجري الشهير بول إردوش (Erdős) — التي تضم مئات الفرضيات المفتوحة منذ عقود — إلى ساحة اختبار جديدة لقدرات الذكاء الاصطناعي، بعد تزايد تقارير تتحدث عن مساهمة نماذج استدلالية في إنتاج براهين لمسائل ظلت عالقة لفترات طويلة، أو في تسريع الوصول إلى حلول كانت مبعثرة في الأدبيات السابقة.
وبينما اعتادت الأوساط العلمية على أن حل المسائل المفتوحة يتطلب شهوراً أو سنوات من العمل البشري، بدأت تظهر نماذج “عمل” مختلفة: ذكاء اصطناعي يقترح مسار برهان، وباحث يراجع ويُنقّح، ثم تأتي مرحلة توثيق الحل بشكل رسمي عبر أدوات “التثبيت” (Formalization) التي تتحقق من سلامة البرهان خطوة بخطوة داخل أنظمة رياضية صارمة.
من “الضجة” إلى القياس العلمي
في الأسابيع الماضية، أشار عالم الرياضيات الشهير تيرينس تاو إلى أن منظومة مسائل إردوش أصبحت تمتلك سياسة “متوازنة” تجاه استخدام الذكاء الاصطناعي: تشجّع الإفصاح عن الاستعانة بالنماذج، لكنها في الوقت نفسه تحذّر من المبالغة في نسب الإنجاز للآلة دون تدقيق علمي كافٍ.
ويُلفت تاو النظر إلى نقطة مهمّة: كثير من مسائل إردوش تقع ضمن ما يصفه البعض بـ“الذيل الطويل” من المشكلات؛ أي مسائل قد تبدو مغمورة أو ليست على واجهة الاهتمام الأكاديمي، لكنها في المقابل قد تمتلك حلولًا مباشرة أو مسارات أقصر مما يُتخيّل—ما يجعلها مناسبة أكثر لأسلوب البحث المنهجي الذي تتفوّق فيه الأنظمة الحاسوبية.
“التثبيت الرسمي”: صمام أمان للبرهان
أحد التحولات التي ترافق صعود الذكاء الاصطناعي في الرياضيات هو ازدياد الاعتماد على أدوات التحقق الرسمي مثل Lean (مساعد إثبات مفتوح المصدر)؛ إذ تسمح هذه الأدوات بتحويل البرهان إلى صيغة قابلة للفحص الآلي، ما يقلّل مساحة الخطأ أو “الثغرات غير المرئية” التي قد تفلت حتى من مراجعات الخبراء.
وتظهر هنا أدوات تجارية/بحثية جديدة مثل “Aristotle” المرتبطة بشركة Harmonic، والتي يَذكر نقاش تقني متداول أنها قد تساعد في ترجمة براهين غير رسمية إلى صياغة Lean كنوع من “التصديق القوي” على أن الفكرة الأساسية متماسكة.
لماذا يهم هذا التحول؟
لأن ما يحدث لا يتعلق فقط بـ“عدد المسائل المحلولة”، بل بتغيّر طريقة إنتاج المعرفة الرياضية نفسها. فبدلاً من نموذج “العالم الفرد” الذي يكتب برهاناً ثم يقدمه للمجتمع العلمي، نحن أمام سلسلة عمل جديدة قد تتكون من:
-
نموذج ذكاء اصطناعي يقترح خطوات وبدائل ومسارات.
-
باحث/فريق بشري يراجع المنطق، ويستبعد الاحتمالات الهشة، ويعيد الصياغة.
-
أداة تثبيت رسمي تتحقق من صحة البرهان آلياً.
هذه الحلقة الثلاثية تقلل زمن التجريب، وتوسّع مساحة الاستكشاف، وتُسرّع الوصول إلى “نسخ قابلة للنشر” من النتائج—مع بقاء الدور البشري جوهرياً في النقد، والتفسير، وربط النتائج بالسياق الأوسع.
حدود الواقع… وحدود الضجة
ورغم الزخم، ما زالت هناك أسئلة مفتوحة:
-
هل حلول الذكاء الاصطناعي “أصيلة” فعلاً أم أنها إعادة تركيب ذكية لأفكار منشورة؟
-
ما معيار نسبة الفضل: للنموذج أم للباحث أم لأداة التثبيت؟
-
وكيف يمكن منع تضخيم ادعاءات الحلول قبل مرورها عبر التحكيم العلمي؟
تيرينس تاو نفسه يلمّح إلى أهمية هذه الأسئلة عبر التشديد على “سياسة الإفصاح” وضرورة التعامل الجاد مع نسب الإنجاز، خصوصاً مع انتشار نماذج قادرة على تقديم براهين “تبدو صحيحة” لكنها تحتاج تدقيقاً صارماً قبل اعتمادها.
إلى أين يتجه المشهد؟
المؤشرات الحالية تقول إن الذكاء الاصطناعي لن “يستبدل” علماء الرياضيات، لكنه سيعيد توزيع الجهد: البشر يركزون أكثر على اختيار المسألة، وتقييم قيمة النتيجة، وصياغة الفكرة الكبرى… بينما تتولى النماذج جزءاً متزايداً من البحث في الفضاء الاحتمالي للحلول، وتوليد المسارات، واختبار الحالات، وتقديم بدائل سريعة.
ومع توسع أدوات التثبيت الرسمي، قد يصبح “التحقق” نفسه أسرع وأكثر شيوعاً، ما يرفع سقف الثقة ويقلل مساحة الجدل حول صحة النتائج—خصوصاً في المسائل التي تتطلب براهين تقنية طويلة.