Lean Confirms Gap in Mochizuki's ABC Conjecture Proof

Gap in Mochizuki's proof of ABC confirmed by Lean

After two years of rigorous analysis, our team concluded that the argument connecting Theorem 3.11 to Corollary 3.12 in Mochizuki's IUT papers cannot be formalized. While Mochizuki's explanations continue to evolve, we reserve final judgment for now. Our LANA project successfully provided a manageable, outsider-written analysis of this critical section, comparing it directly with the 2018 Scholze-Stix report to clarify the situation for the broader mathematical community.

"The way the argument from Theorem 3.11 to Corollary 3.12 is written in the IUT papers is unformalizable."