How to Believe a Machine-Checked Proof

Robert Pollack

July 1997


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.


Last modified: 2003-06-08 by webmaster.