As a PhD student in Programming Languages, can I request a reference?* Nobody managed to provide one on MathOverflow, and that's the StackExchange for professional mathematicians:
https://mathoverflow.net/q/226966/36016
Of course, your claim is vacuously true, since you can add a trace of all steps of a proof verifier. It's also vacuously true because you can add a dump of the Internet to the proof. Neither thing is insightful.
> what we normally think of as an "honest proof" is a series of steps each of which follows from the previous by application of one of a finite number of axioms or rules of deduction, and such an "honest" proof is thus checkable in linear time by checking each step
Also, for the record: actual formal proofs for (say) standard ZFC are exponentially bigger than anything you want to work with.
EDIT: To clarify, I didn't mean to imply I'm some authority, just to suggest I'm not so obviously* an idiot. Which was maybe stupid anyway.
[1]: https://en.wikipedia.org/wiki/Method_of_analytic_tableaux
/dodge
- The proof will turn out to have a flaw
- The flaw will not be that hard to find (though probably not completely trivial; but rather of the kind: it takes much time to go to the details of the proof arguments)
- The flaw will not be interesting in itself and will not advance the field
> ...this guy is an established senior researcher at the University of Bonn
I make more mistakes by 09:00 than most people will make all day. Hell, my girlfriend would suggest that we can move that time forward a couple of hours.