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