> 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.)
He may be saying the equivalent of "A computer won't help you to prove that 1+1=3“