>It's similar to Mochizuki claiming to have proved the ABC conjecture

Now I wonder if someone could port his proof to Lean