Lean confirma una brecha en la demostración de la conjetura ABC de Mochizuki
Gap in Mochizuki's proof of ABC confirmed by Lean
El proyecto LANA, liderado por el matemático Fumiharu Kato, anunció en una conferencia de prensa que el argumento que conecta el Teorema 3.11 con el Corolario 3.12 en los artículos de la Teoría IUT de Mochizuki es imposible de formalizar tal como está escrito. Sin embargo, dado que la explicación de Mochizuki ha evolucionado recientemente, el equipo reserva su juicio final. LANA también presentó un análisis accesible del argumento crítico para el público matemático general, incluyendo una comparación con el informe de Scholze-Stix de 2018.
La forma en que está escrito el argumento del Teorema 3.11 al Corolario 3.12 en los artículos de IUT es informalizable.