> Definitions went on for pages, followed by theorems whose statements were similarly long, but whose proofs only said, essentially, “this follows immediately from the definitions.”
This sounds perfect for machine checked proofs, but I guess the proofs are actually a lot more involved than they are presented.
>One final point: I get very annoyed by all references to computer-verification (that came up not on this blog, but elsewhere on the internet in discussions of Mochizuki’s work). The computer will not be able to make sense of this step either. The comparison to the Kepler conjecture, say, is entirely misguided: In that case, the general strategy was clear, but it was unclear whether every single case had been taken care of. Here, there is no case at all, just the claim “And now the result follows”.
What does that mean, then? That a leap is being made that depends on the reader's fuzzy intuitions, rather than the established axioms? If that's the case, it's not a formal proof at all, no?
Or am I way off here?
> Any proof that can be spelled out at a level of detail sufficient to be analyzed by a computer is necessarily going to consist entirely of steps that are each completely comprehensible to a mathematician.
This means there must either be a lot of steps or a lot of different paths to follow in order for a computer to be of use. Neither is the case here.
He may be saying the equivalent of "A computer won't help you to prove that 1+1=3“
But it can. You need to have the computer 'comprehend' the relevant axioms, of course.
If your 'proof' is in fact just arguing the case for new axioms, that isn't a proof at all, it's a misunderstanding of what 'axiom' means. (They're definitions, not profound universal truths.)
Here Scholze is saying that part of the proof simply hasn't been written, so there's nothing to verify. I think he's missing that computer verification proponents are also aware of that and are either
1. trying to motivate the camp that claims to understand Mochizuki's work to formalize and computer-verify it
and/or
2. suggesting that some of the gaps can be filled in by automatic theorem provers
The problem is that these papers are vague. The translation to computerized version would be a very different thing, it'd require a lot of creative writing on behalf of the translator.