Les efforts visant à vérifier une preuve controversée de la conjecture ABC à l'aide d'un logiciel informatique n'ont pas abouti. Un rapport intermédiaire du projet Lean and Anabelian Geometry montre que les mathématiciens restent divisés sur la validité de la théorie sous-jacente.
En 2012, Shinichi Mochizuki, de l'université de Kyoto, a présenté une preuve de 500 pages de la conjecture ABC. Cette démonstration repose sur sa théorie inter-universelle de Teichmüller, que peu de mathématiciens ont été en mesure de vérifier.
Un projet baptisé LANA a tenté de formaliser cette preuve dans le langage de programmation Lean. Son récent rapport intermédiaire indique que les membres ont eu des discussions animées, mais ne sont pas parvenus à un consensus sur la solidité de la théorie.
Le rapport souligne les problèmes persistants soulevés dès 2018 par Peter Scholze et Jakob Stix. Abhishek Saha, de l'université Queen Mary de Londres, a déclaré que ce résultat confirme l'opinion de la plupart des mathématiciens selon laquelle il existe une faille sérieuse dans la théorie.
Ivan Fesenko, de l'université de Westlake, soutient que ces critiques sont déplacées et qu'une preuve formalisée finira par voir le jour.