باحثون من معهد ماساتشوستس للتكنولوجيا (MIT) يُنالون منحًا رائدة في مجال الذكاء الاصطناعي لتعزيز الاكتشاف الرياضي، ضمن مبادرة "الذكاء الاصطناعي من أجل الرياضيات" التي أطلقتها مؤسسة ريناسانس فلانتروبي وشركة XTX Markets. من بين الفائزين، الباحثان ديفيد روي (خريج 2006) وأندرو سوثيرلاند (خريج 1990، دكتوراه 2007) من قسم الرياضيات في MIT، اللذان يتعاونان مع كريس بيركبيك من جامعة إيست أنغليا، لتطوير أدوات تُعزز إثبات النظريات التلقائي من خلال ربط قاعدة بيانات LMFDB، التي تُعدّ "مكتبة معرفية" ضخمة في نظرية الأعداد، بمنصة Lean4 وكتابتها الرياضية المفتوحة (mathlib). تُعدّ هذه المنحة جزءًا من 29 مشروعًا مُختارة، تهدف إلى دعم الباحثين في جامعات ومنظمات حول العالم لتطوير أنظمة ذكاء اصطناعي تُسهم في تسريع التقدم في الرياضيات. يُبرز سوثيرلاند أن أدوات إثبات النظريات التلقائيّة، رغم تعقيدها التقني، تعاني من نقص في التمويل، لكن تطورات الذكاء الاصطناعي، خاصة نماذج اللغة الكبيرة (LLMs)، بدأت تخفض الحواجز التقنية، مما يجعل هذه الأدوات متاحة الآن لعلماء الرياضيات العاملين في الميدان. mathlib هي مكتبة رياضية ضخمة تُبنى بمشاركة جماعية، وتُستخدم في نظام Lean، وهو نظام رسمي يتحقق من صحة كل خطوة في البرهان. تضمّ هذه المكتبة حاليًا نحو 100 ألف نتيجة رياضية، بينما تضم LMFDB أكثر من 100 مليون بيان محدّد في مجالات نظرية الأعداد. ويُعدّ سوثيرلاند وروي من المحرّرين الرئيسيين في LMFDB. الهدف من المشروع هو بناء أدوات تسمح بتسخير LMFDB مباشرة من داخل mathlib، مما يُمكّن الأدوات المساعدة في البرهان من الوصول إلى كمّ هائل من المعرفة غير المُصاغة رياضيًا، دون الحاجة إلى ترجمة كل البيانات مسبقًا. وفقًا لروي، فإن هذا النهج يُعدّ أداة قوية للاكتشاف الرياضي، لأن عدد الحقائق التي قد يرغب عامل الذكاء الاصطناعي في استعراضها أثناء البحث عن برهان يفوق بكثير عدد الحقائق التي يجب تأسيسها فعليًا في البرهان. كما يُشير الباحثون إلى أن إثبات نظريات حديثة غالبًا ما يعتمد على عمليات حسابية معقدة، مثل "الخدعة الثلاثة-خمسة" التي استخدمها أندرو ويلز في إثبات نظرية فيرما الأخيرة. وباستخدام النتائج المُخزّنة مسبقًا، يُستفيد من آلاف سنوات من وقت المعالجة الحاسوبية التي تم استثمارها في بناء LMFDB، مما يوفر تكاليف هائلة ويجعل من الممكن البحث عن أمثلة أو معاكسات دون الحاجة إلى تحديد نطاق البحث مسبقًا. كما يُبرز سوثيرلاند أن التصنيف الدقيق للبيانات، كمثلاً تأكيد دور "المُعامل" (conductor) في منحنيات إيليبتيك، ساهم في اكتشاف رياضي بارز باستخدام أدوات التعلم الآلي، يُعرف بـ"المُرَمَّرَات" (murmurations). ويتطلع الفريق إلى تشكيل فريق عمل، والتفاعل مع مجتمعات LMFDB وmathlib، وبدء تأسيس التعريفات الأساسية المتعلقة بالمنحنيات الإيليبتيك، الحقول العددية، والأشكال المودولية، مع تمكين عمليات بحث LMFDB داخل mathlib. ودعا روي طلاب MIT المهتمين بالمشاركة إلى التواصل مع الفريق، مؤكدًا أن هذه المبادرة تمثل فرصة فريدة لدمج التكنولوجيا الحديثة مع التقدم في الرياضيات.