Gap in Mochizuki's proof of ABC confirmed by Lean

In today's press conference, we explained our efforts over the last two years which resulted in the following conclusion: The way the argument from Theorem 3.11 to Corollary 3.12 is written in the IUT papers is unformalizable. But since Mochizuki's explanation of this point has