قد يتم حل خلاف دام عقدًا في الرياضيات حول إثبات شينيتشي موتشيزوكي لتخمين ABC باستخدام التحويل الحاسوبي الرسمي. اقترح موتشيزوكي ترجمة عمله الذي يبلغ 500 صفحة إلى لغة البرمجة Lean للتحقق الآلي. يمكن لهذا النهج أن يجسر الفجوات بين المعسكرات المتضاربة في المجتمع الرياضي.
يعود الخلاف إلى عام 2012، عندما نشر شينيتشي موتشيزوكي، أستاذ في جامعة كيوتو في اليابان، إثباتًا واسعًا يبلغ 500 صفحة لتخمين ABC. يتعلق هذا المشكلة البالغة من العمر 40 عامًا بالمعادلة a + b = c للأعداد الصحيحة الكاملة والعلاقات بين عواملها الأولية، مع آثار على نظريات مثل آخر نظرية فيرمات. يعتمد إثبات موتشيزوكي على نظريته المعقدة لتايخ مولر بين الكوني (IUT)، التي وجد الكثير من الخبراء صعوبة في فهمها.
انخفض الحماس الأولي مع توقف جهود التحقق. في عام 2018، حدد بيتر شولز من جامعة بن في ألمانيا وجاكوب ستيكس من جامعة غوته في فرانكفورت خطأ محتملًا، نفاه موتشيزوكي. بدون سلطة مركزية، انقسم عالم الرياضيات: معظم الرياضيين في جانب واحد، ومجموعة أصغر مرتبطة بموتشيزوكي ومعهد البحوث في العلوم الرياضية في كيوتو في الجانب الآخر.
لكسر الجمود، يدعو موتشيزوكي الآن إلى تحويل الإثبات إلى Lean، لغة للرياضيات المفحوصة حاسوبيًا. مستوحى من مؤتمر في يوليو في طوكيو، يجادل في تقرير حديث بأن Lean يمكن أن يحرر الحقيقة الرياضية من "الديناميكيات الاجتماعية والسياسية". كما يكتب: "[Lean] هي أفضل التكنولوجيا وربما الوحيدة... لتحقيق تقدم معنوي فيما يتعلق بالهدف الأساسي لتحرير الحقيقة الرياضية من نير الديناميكيات الاجتماعية والسياسية."
يرى الخبراء إمكانية لكن يحذرون. يقول كيفن بوزارد من كلية إمبريال لندن: "إذا كُتب في Lean، فهو ليس جنونًا، أليس كذلك؟ الكثير من المحتوى في الأوراق مكتوب بلغة غريبة جدًا، لكن إذا استطعت كتابتها في Lean، فهذا يعني أن هذه اللغة الغريبة على الأقل أصبحت شيئًا محددًا تمامًا." يضيف يوهان كوملين من جامعة أوترخت: "نريد فهم السبب [في IUT]، وقد انتظرنا ذلك لأكثر من 10 سنوات. يمكن لـ Lean أن يساعدنا في فهم تلك الإجابات."
ومع ذلك، المهمة هائلة، تتطلب فرقًا من المتخصصين وربما سنوات من العمل. حتى النجاح قد لا ينهي المناقشات حول التفسير، كما يعترف موتشيزوكي بأن Lean لا يقدم "علاجًا سحريًا" للمشكلات الاجتماعية. يظل بوزارد متفائلًا: "لا يمكنك الجدال مع البرمجيات."