ماذا يحدث عندما يبدأ الذكاء الاصطناعي في التحقق من عمل علماء الرياضيات؟

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

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

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

حول دعم الصحافة العلمية

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

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

لغز التعبئة

في عام 2016، أصبحت فيازوفسكا شخصية محورية في الرياضيات من خلال حل لغز عمره عقود: كيف يمكن ترتيب المجالات بأكثر الطرق كفاءة في استخدام المساحة؟ للعثور على الحل الوحيد الأكثر كفاءة من حيث المساحة، يجب عليك أولاً أن تثبت أن جميع الترتيبات الكروية الأخرى التي لا حصر لها تتطلب مساحة أكبر. استغرق الأمر حتى عام 1998 لإثبات أن الترتيب على شكل هرم – مثل كومة من البرتقال في السوبر ماركت – هو بالفعل الخيار الأكثر كثافة في الفضاء ثلاثي الأبعاد.

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

كانت أول من تناولت إثبات الفضاء الثماني الأبعاد، وحصلت عليه على وسام فيلدز عام 2022. أقنعها زميلها هنري كوهن، عالم الرياضيات في معهد ماساتشوستس للتكنولوجيا، بالتعاون مع العديد من المتعاونين – بما في ذلك ستيفن ميلر من جامعة روتجرز، ودانيلو رادشينكو، الذي يعمل الآن في معهد الدراسات العلمية المتقدمة، وأبيناف كومار، الذي كان يعمل آنذاك في جامعة ستوني بروك – لتطوير دليل على الفضاء ذي الـ 24 بُعدًا. وفي غضون أسبوع نجحوا.

ولكن هل يمكن إضفاء الطابع الرسمي على هذه الأدلة والتحقق منها بواسطة الكمبيوتر؟ في عام 2023، التقت فيازوفسكا بسيدهارث هاريهاران، الذي كان حينها يدرس للحصول على درجة الماجستير في الرياضيات في إمبريال كوليدج لندن ويعمل مع عملية إضفاء الطابع الرسمي تسمى Lean. وبدأوا بتبادل الأفكار. ويقول: “كنا مجرد شخصين فضوليين يريدان تعلم شيء ما، وهذه هي الطريقة التي بدأ بها الأمر”.

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

وفي الوقت نفسه، عالم الرياضيات أوغست بويروكس، دكتوراه. ساعد أحد الطلاب في المعهد الفيدرالي السويسري للتكنولوجيا في لوزان، في إطلاق شركة Math, Inc. الناشئة في أواخر صيف عام 2025. ويشرح بورو قائلاً: “نريد أن نجعل من الممكن نقل محتوى ورقة أو كتاب تلقائيًا إلى رمز Lean والتحقق منه على الفور”.

أصبحت شركة Math, Inc.‎ على علم بالمشروع الذي قام به هاريهاران وزملاؤه وأجرت اتصالات. يتذكر هاريهاران، وهو الآن حاصل على درجة الدكتوراه: “في خريف عام 2025، أخبرنا العاملون في Math, Inc. أنهم تمكنوا من إضفاء الطابع الرسمي على أجزاء أصغر من مشروعنا وشاركوا بعض نتائجهم معنا”. طالب في جامعة كارنيجي ميلون. “ثم توقف الاتصال. ولم نكن نعرف إلى أي مدى وصلوا – أو حتى إذا كانوا لا يزالون يعملون على ذلك.”

يقول بوارو: “كنا فريقًا صغيرًا جدًا”. “لقد أدركنا أننا لا نستطيع تحسين نظامنا والعمل على مشروع هاريهاران في نفس الوقت. لذلك ركزنا على الذكاء الاصطناعي.” في الأسابيع التالية، قام أعضاء فريق Math, Inc. بتطوير نموذج اللغة القائم على الوكيل، والذي يسمى Gauss.

في النهاية، بدا البرنامج قادرًا على ترجمة العمل الرياضي إلى كود Lean والتحقق منه تلقائيًا دون تدخل بشري. يقول بورو: “لقد أخذنا برهان فيازوفسكا الثماني الأبعاد كاختبار”. “وفجأة، قام النظام بإخراج الدليل الرسمي بالكامل. لقد فاجأنا ذلك تمامًا.”

مستقبل الرياضيات

كان بوارو وزملاؤه يشعرون بسعادة غامرة. ولم يشعر فريق هاريهاران بنفس الشعور. يقول هاريهاران: “كنا، على أقل تقدير، مندهشين للغاية”. “لقد كان مشروعنا؛ لقد بذلنا الكثير من العمل فيه على مدار عامين، ثم قامت شركة Math, Inc.‎ بحل المشكلة.”

خطط هاريهاران وزملاؤه لأن يكون جزء من عملية إضفاء الطابع الرسمي أساسًا لأطروحة الطالب الجامعية. يقول هاريهاران: “ولكن أعتقد أن الأمر هكذا. فالذكاء الاصطناعي أمر مدمر”.

يقول بوارو: “في خضم الإثارة، لم نفكر بشكل كامل في العواقب”. “أفهم أنه من الخارج، ربما بدا الأمر كما لو أننا تعمدنا الحفاظ على سرية التقدم الذي أحرزناه. ومن المؤكد أننا سنكون أكثر حذراً في المستقبل”.

ثم تناولت شركة Math, Inc.، برهان Viazovska الثاني، والذي تناول التعبئة المثالية للكرة في 24 بُعدًا. يقول بوارو: “في هذه الحالة، أعطينا غاوس الورقة فقط، وليس أي شيء آخر”. “وقام النظام بتحويلها إلى حوالي 120 ألف سطر من التعليمات البرمجية اللينة.” وقد تم التحقق من الرمز منذ ذلك الحين.

تتعاون شركة Math, Inc.‎ الآن مع Hariharan وخبراء آخرين لتعزيز عملية الصياغة التلقائية وتغطية المزيد من الرياضيات. يقول بوارو: “بالنسبة للعديد من المناطق، لا تزال العناصر الأساسية مفقودة في نهج لين – لم نتمكن من إضفاء الطابع الرسمي على الأدلة (في تلك المناطق) في الوقت الحاضر”.

عندما يصبح من الممكن إضفاء الطابع الرسمي على أجزاء كبيرة من الرياضيات، ستفتح إمكانيات جديدة. إن أنظمة شركة Math, Inc. هي أكثر من مجرد آلات ترجمة: فهي يمكنها اكتشاف الأخطاء البسيطة في الأوراق وتصحيحها، وتشير هذه القدرة إلى مستقبل محتمل تشرف فيه أنظمة الذكاء الاصطناعي المتفوقة على جميع الرياضيات – وربما تتفوق على البشر في الأبحاث.

يقول بورو: “عندما تفهم نماذجنا الرياضيات في مجملها، يمكنها التفكير فيها بطريقة مختلفة تمامًا، ومن المحتمل أن تقدم نتائج جديدة تمامًا”.

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