Perselisihan selama satu dekade dalam matematika mengenai bukti konjektur ABC oleh Shinichi Mochizuki mungkin dapat diselesaikan menggunakan formalisasi komputer. Mochizuki menyarankan menerjemahkan karya 500 halamannya ke dalam bahasa pemrograman Lean untuk verifikasi otomatis. Pendekatan ini dapat menjembatani perpecahan antara kubu-kubu yang bertentangan dalam komunitas matematika.
Kontroversi ini berakar pada tahun 2012, ketika Shinichi Mochizuki, seorang profesor di Universitas Kyoto di Jepang, menerbitkan bukti sepanjang 500 halaman untuk konjektur ABC. Masalah berusia 40 tahun ini berkaitan dengan persamaan a + b = c untuk bilangan bulat utuh dan hubungan di antara faktor prima mereka, dengan implikasi untuk teorema seperti Teorema Terakhir Fermat. Bukti Mochizuki bergantung pada teori Teichmüller antar-universal (IUT) yang rumitnya, yang banyak ahli temukan sulit untuk dipahami.
Antusiasme awal mereda saat upaya verifikasi terhenti. Pada 2018, Peter Scholze dari Universitas Bonn dan Jakob Stix dari Universitas Goethe Frankfurt mengidentifikasi cacat potensial, yang Mochizuki bantah. Tanpa otoritas pusat, dunia matematika terbelah: sebagian besar matematikawan di satu sisi, dan kelompok kecil yang berafiliasi dengan Mochizuki dan Institut Penelitian Ilmu Matematika Kyoto di sisi lain.
Untuk memecah kebuntuan, Mochizuki kini menganjurkan formalisasi bukti dalam Lean, bahasa untuk matematika yang diperiksa komputer. Terinspirasi oleh konferensi Juli di Tokyo, ia berargumen dalam laporan terbaru bahwa Lean dapat membebaskan kebenaran matematika dari "dinamika sosial dan politik." Seperti yang ia tulis, “[Lean] adalah teknologi terbaik dan mungkin satu-satunya… untuk mencapai kemajuan yang bermakna terkait tujuan mendasar membebaskan kebenaran matematika dari kuk dinamika sosial dan politik.”
Para ahli melihat potensi tetapi berhati-hati. Kevin Buzzard dari Imperial College London mencatat, “Jika ditulis dalam Lean, maka itu bukan hal gila, kan? Banyak hal dalam makalah ditulis dalam bahasa yang sangat aneh, tapi jika Anda bisa menulisnya dalam Lean, maka setidaknya bahasa aneh itu menjadi sesuatu yang sepenuhnya terdefinisi dengan baik.” Johan Commelin dari Universitas Utrecht menambahkan, “Kami ingin memahami mengapa [IUT], dan kami telah menunggu itu selama lebih dari 10 tahun. Lean dapat membantu kami memahami jawaban-jawaban itu.”
Namun, tugasnya sangat besar, memerlukan tim spesialis dan mungkin bertahun-tahun kerja. Bahkan kesuksesan mungkin tidak mengakhiri perdebatan tentang interpretasi, karena Mochizuki mengakui Lean tidak menawarkan "obat ajaib" untuk isu sosial. Buzzard tetap optimis: “Anda tidak bisa berdebat dengan perangkat lunak.”