="Henry Baker" <hbaker1@pipeline.com> The reason why human proofs may not be so trivial to check is that we rely on thousands or tens of thousands of trivial lemmas and also leave out lots of intermediate steps that need to be filled in by intelligence.
Exactly. So who or what is going to create suitable proofs [*], and how? I doubt humans are going to create suitable proofs directly; what they do now is hard enough! So either the proof will be found mechanically in the first place (hard) or some mechanism is going to generate it from less formal human input (also hard). It's like the old "ham & eggs" joke: If we had Wikiproofia, we could check submitted proofs in linear time, if we had mechanically checkable proofs. -------- [*] In elementary school they called these "demonstrations", in contrast to the usual "natural language" proofs. Is that correct modern nomenclature?