Gap in Mochizuki's proof of ABC confirmed by Lean

Other: mathematics research(twitter.com)view on HackerNews
IUTmathematicsresearchverificationprooftheoremcorollaryMochizukiScholze-Stixreportcomputer-assisted verification.

Author: ogogmad

Date: 7/18/2026

Article Summary:
A press conference was held to discuss the IUT (Inter-universal Teichmüller theory) papers, specifically the argument from Theorem 3.11 to Corollary 3.12, which was deemed unformalizable.