[336f5]

It also sounds like a motivating example for machine-checked proofs: if one could feed Mochizuki's proof into Coq or something and be assured that it was correct, even if only in a purely formal sense, I suspect there would be much more interest in grappling with the concepts to understand what the proof is doing, whether it's acceptable, and why the proof is correct. As it stands, there's the risk of a wild goose chase.

[jordigh]

If Mochizuki were able to write a machine-checkable proof, he would also be able to write a human-checkable proof, which is far easier to write.

[kinghajj]

Well, supposedly he did write a human-checkable proof--it's just that the reviewer must be familiar with several of his novel ideas. Like any human-intended proof, there's an assumption of foreknowledge.