Upaya untuk memverifikasi pembuktian kontroversial konjektur ABC menggunakan perangkat lunak komputer tidak membuahkan hasil. Laporan sementara dari proyek Lean and Anabelian Geometry menunjukkan bahwa para matematikawan masih terpecah mengenai validitas teori yang mendasarinya.
Pada tahun 2012, Shinichi Mochizuki dari Universitas Kyoto mempresentasikan pembuktian konjektur ABC setebal 500 halaman. Pembuktian tersebut mengandalkan teori Inter-universal Teichmüller miliknya, yang hanya sedikit matematikawan mampu memverifikasinya.
Sebuah proyek yang dikenal sebagai LANA telah mencoba memformalkan pembuktian tersebut ke dalam bahasa pemrograman Lean. Laporan sementara terbarunya menyatakan bahwa para anggota telah melakukan diskusi yang hidup namun gagal mencapai konsensus mengenai apakah teori tersebut valid.
Laporan tersebut menyoroti masalah berkelanjutan yang pertama kali diangkat pada tahun 2018 oleh Peter Scholze dan Jakob Stix. Abhishek Saha dari Queen Mary University of London mengatakan hasil tersebut sesuai dengan pandangan sebagian besar matematikawan bahwa terdapat celah serius dalam teori itu.
Ivan Fesenko dari Universitas Westlake berpendapat bahwa kritik tersebut tidak tepat dan pembuktian yang diformalkan pada akhirnya akan muncul.