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