Record Details

How to Believe a Machine-Checked Proof

BRICS Report Series

View Archive Info
 
 
Field Value
 
Title How to Believe a Machine-Checked Proof
 
Creator Pollack, Robert
 
Description 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 inFLT? I start from the position that you must have some personal experience of understanding to attain belief, and to have this experience you must engage your intuition and other mental processes which are impossible to formalise. By machine-checked proof I mean a formal derivation in some given formalsystem; I am talking about derivability, not about truth. Further, I want to talk about actually believing an actual formal proof, not about formal proofs in principle; to be interesting, any approach to this problem must be feasible. You might try to read my proof, just as you would a proof in a journal; however,with the current state of the art, this proof will surely be too long for you to have confidence that you have understood it. This paper presents a technologicalapproach 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. The approach is not entirely successful philosophically as there seems to be a fundamental difference between machine checked mathematics,which depends on empirical knowledge about the physical world, and informal mathematics, which needs no such knowledge (see section 3.2.2).In the rest of this introduction I outline the approach and mention related work. In following sections I discuss what we expect from a proof, add details to the approach, pointing out problems that arise, and concentrate on what I believeis the primary technical problem: expressiveness and feasibility for checking of formal systems and representations of mathematical notions.
 
Publisher Aarhus University
 
Date 1997-01-18
 
Type info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion
 
Format application/pdf
 
Identifier https://tidsskrift.dk/brics/article/view/18945
10.7146/brics.v4i18.18945
 
Source BRICS Report Series; No 18 (1997): RS-18 How to Believe a Machine-Checked Proof
BRICS Report Series; Nr. 18 (1997): RS-18 How to Believe a Machine-Checked Proof
1601-5355
0909-0878
 
Language eng
 
Relation https://tidsskrift.dk/brics/article/view/18945/16584