="Henry Baker" <hbaker1@pipeline.com> mechanically _check_ submitted proofs
I agree this is a good idea, but have wondered how far off the dream is. To get a sense of this, I considered some simple concrete cases, such as making mechanically checkable versions of familiar proofs of things like: The game of Hex cannot end in a draw, and in fact is a 1st player win. The number of partitions of N into distinct parts equals that of N into odd parts. Contemporary proofs generally consist of prose designed to convince human readers, with backgrounds somewhat comparable to the authors', of the validity of the thesis. They rely on a vast foundation of common sense and shared context, much as other natural language understanding does. Checking the prose that currently is accepted as a proof seems as challenging as passing a Turing test, or at least understanding a news report. For example with Hex we normally start already knowing what "game" and "draw" mean, and can quickly get concepts like "connected path of cells" and see right away how those paths can be geometrically mutually exclusive, and then finally grok "strategy stealing". But then, given that the validation of any "natural proof" must rely on this considerable hidden context, why would we think we can really trust that a proof checks out just because HAL 9000 says it's OK? On the other hand we could instead try to place a greater burden of proof on the authors to express their arguments in a more formal way. However to avoid vast amounts of redundant effort an investment in building up a sharable semantic infrastructure would be needed. For example we could create standard libraries of formal definitions of things like "game" and "path" so each proof doesn't require complete wheel reinvention. But this seems more or less equivalent to capturing the shared foundation that natural language discourse depends on, so it's not clear requiring more formality would really reduce the overall effort needed. Is Wikiproofia's first customer release date inevitably post-singularity?