|
How to Believe a Machine-Checked Proof
Robert Pollack July 1997 |
Abstract:Suppose I say ``Here is a machine-checked proof of Fermat's last theorem (FLT)''. How can you use my putative machine-checked proof as evidence for belief in FLT? This paper presents a technological approach for reducing the problem of believing a formal proof to the same psychological and philosophical issues as believing a conventional proof in a mathematics journal. I split the question of belief into two parts; asking whether the claimed proof is actually a derivation in the claimed formal system, and then whether what it proves is the claimed theorem. The first question is addressed by independent checking of formal proofs. I discuss how this approach extends the informal notion of proof as surveyable by human readers, and how surveyability of proofs reappears as the issue of feasibility of proof-checking. The second question has no technical answer; I discuss how it appears in verification of computer systems
Available as PostScript, PDF, DVI. |