En 2012 fue noticia la supuesta demostración de la conjetura abc del matemático japonés Shinichi Mochizuki (Universidad de Kioto, Japón). En 2018, Peter Scholze (Medalla Fields en 2018) y Jakob Stix mostraron un grave error en el argumento que lleva del teorema 3.11 al corolario 3.12, concluyendo que la demostración es incorrecta. En 2026 ningún japonés ha logrado resolver el error (fuera de Japón todo el mundo sabe que el error es definitivo). En 2023 nació el proyecto LANA (Lean for ANAbelian geometry) del japonés Centro de Matemáticas ZEN (ZMC). Su objetivo era verificar de forma automática en Lean la (supuesta) demostración de Mochizuki, lo que requiere desarrollar una librería en Lean con toda la geometría anabelina y la teoría de Teichmüller interuniversal (IUT). El 20 de julio de 2026 se ha publicado su primer informe oficial de resultados. Como era de esperar, tras dos años de duro trabajo, el proyecto LANA está atascado en la transición del teorema 3.11 al corolario 3.12. No hay ninguna esperanza de poder avanzar.

El proyecto LANA no puede afirmar que Scholze y Stix tengan razón. Ningún japonés del entorno de Mochizuki dará su brazo a torcer. De hecho, no se cortan afirmando el argumento de Scholze y Stix es incorrecto, en la línea de la crítica de de Mochizuki. Pero hay un problema mucho mayor, la transición del teorema 3.11 al corolario 3.12 no es formalizable en Lean. Cual coyote en el precipicio del teorema 3.11, Mochizuki caminó por el aire sin caer hacia abajo, retornando a tierra firme con el corolario 3.12. Lean no permite incumplir con la ley de la gravedad. El coyote Mochizuki vuelve a perder ante el correcaminos Scholze. Las matemáticas kiotenses tendrán que aprender a convivir con el escarnio de haber apoyado a ciegas a Mochizuki y publicado su demostración sin revisión por pares externa (LCMF, 03 abr 2020). El heredero japonés de Grothendieck, según Labatut en «Un verdor terrible» (2020), quedará marcado para siempre por su soberbia al reconocer su error.

El informe del LANA Project, «Project LANA interim report on IUT theory,» GitHub, 20 Jul 2026 [PDF] (50 páginas) solo tiene interés para los aficionados a la historia de las matemáticas (hay rueda de prensa en su canal de YouTube). Sin embargo, como en la actualidad está de moda el papel de la inteligencia artificial en las matemáticas, siendo la prueba definitiva la verificación automática usando Lean, quizás conviene recordar que solo una pequeña parte de las matemáticas está formalizada en Lean. Baste recordar que sigue en curso el proyecto FLT (Fermat’s Last Theorem Project), cuyo objetivo es verificar la demotración de Andrew Wiles (y Richard Taylor); se inició en 2023 y pretende acabar en 2029, por ahora no ha encontrado ningún problema, pero no es tarea baladí.

El llamado hexágono de Scholze y Stix es una representación de ciertas identidades entre espacios usados en IUT. Dicho diagrama no conmuta, es decir, los dos recorridos de las flechas difieren en cierto factor. El problema es que al introducir dicho factor para restaurar la conmutatividad se arruina la desigualdad diofántica necesaria para deducir la conjetura abc. Mochizuki respondió que dicho hexágono es irrelevante en su demostración y que no se requiere su conmutatividad. Por desgracia, su réplica vehemente no convenció a la comunidad matemática internacional.

El problema encontrado por el proyecto LANA es diferente (aunque en esencia es el mismo). El teorema 3.11 proporciona un algoritmo que reconstruye mediante métodos anabelianos una familia de salida posibles.  Una de ellas es la que se usa como entrada en el corolario 3.12. Con la formalización se logra esquivar que en dicha entrada dos espacios sean isomorfos (pues no lo son), pero se relaja la condición a que al menos sean compatibles (en cierto sentido). Por desgracia, Lean no permite que sean compatibles espacios que son incompatibles (en dicho sentido). Por ello, el paso del teorema 3.11 al corolorio 3.12 no se puede formalizar en Lean. Así LANA le da la razón a Mochizuki, el hexágono de Scholze y Stix es irrelevante, pero también la da razón a Scholze y Stix, la demostración es incorrecta en el punto donde ellos han identificado que lo era. El proyecto LANA reconcilia la matemática japonesa (o al menos, kiotense) con el resto de la matemática mundial.

Por supuesto, la sombra de Mochizuki planea sobre el proyecto LANA. Su informe no dice que sea imposible formalizar lo que parece imposible de formalizar. El proyecto sigue en curso, intentando superar la obstrucción que impide completar la formalización. No sabemos cuánto se alargará la agonía, pero la búsqueda de una reformulación que permita superar la objección lógica continúa. En mi opinión, la búsqueda será vana.