[peq]

Mathematicians should do more computer verifiable proofs to avoid discussions like this.

> 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.

[cycrutchfield]

Per Peter Scholze (from https://galoisrepresentations.wordpress.com/2017/12/17/the-a...):

>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”.

[trevyn]

Well that's sort of the point, isn't it? If you can't make the computer make sense of it, you have no proof.

[MaxBarraclough]

> The computer will not be able to make sense of this step either.

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?

[MauranKilom]

I find his explanation of the reverse quite clear:

> 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.

[konschubert]

Maybe he says that the computer won't help understand the proof since the proof is missing a step.

He may be saying the equivalent of "A computer won't help you to prove that 1+1=3“

[MaxBarraclough]

> 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.)

[heinrichhartman]

Exactly, this is how I read it as well.

[cxseven]

For the Kepler Conjecture, human mathematicians first found a way to show that it could be proved by checking a finite (but long) list of computer-verifiable claims.

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

[cycrutchfield]

It took like a decade to produce a computer verified proof for the Kepler Conjecture. And that was just for a relatively well-defined exhaustive search. That sounds like a molehill compared to Mochizuki’s Everest of a proof.

[pas]

Methods have improved a lot since then.

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.