Um esforço para verificar uma controversa prova da conjectura ABC usando software de computador não apresentou progresso. Um relatório preliminar do projeto Lean and Anabelian Geometry mostra que os matemáticos continuam divididos sobre a validade da teoria subjacente.
Em 2012, Shinichi Mochizuki, da Universidade de Kyoto, apresentou uma prova de 500 páginas da conjectura ABC. A prova baseia-se em sua teoria Teichmüller Inter-universal, que poucos matemáticos conseguiram verificar.
Um projeto conhecido como LANA tentou formalizar a prova na linguagem de programação Lean. Seu recente relatório preliminar afirma que os membros realizaram discussões animadas, mas não chegaram a um consenso sobre se a teoria se sustenta.
O relatório destaca questões contínuas levantadas pela primeira vez em 2018 por Peter Scholze e Jakob Stix. Abhishek Saha, da Queen Mary University of London, disse que o resultado corresponde à visão da maioria dos matemáticos de que existe uma falha grave na teoria.
Ivan Fesenko, da Universidade Westlake, sustenta que a crítica é equivocada e que uma prova formalizada eventualmente surgirá.