Un esfuerzo para verificar una controvertida demostración de la conjetura ABC mediante software informático no ha logrado avances. Un informe provisional del proyecto Lean and Anabelian Geometry muestra que los matemáticos siguen divididos sobre la validez de la teoría subyacente.
En 2012, Shinichi Mochizuki, de la Universidad de Kioto, presentó una demostración de 500 páginas de la conjetura ABC. La demostración se basa en su teoría de Teichmüller interuniversal, que pocos matemáticos han podido verificar.
Un proyecto conocido como LANA ha intentado formalizar la demostración en el lenguaje de programación Lean. Su reciente informe provisional indica que los miembros mantuvieron debates animados, pero no lograron llegar a un consenso sobre si la teoría es correcta.
El informe subraya los problemas persistentes planteados por primera vez en 2018 por Peter Scholze y Jakob Stix. Abhishek Saha, de la Universidad Queen Mary de Londres, afirmó que el resultado coincide con la opinión de la mayoría de los matemáticos de que existe una laguna importante en la teoría.
Ivan Fesenko, de la Universidad de Westlake, sostiene que las críticas están fuera de lugar y que, eventualmente, aparecerá una demostración formalizada.