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