How to Believe a Machine-Checked Proof
DOI:
https://doi.org/10.7146/brics.v4i18.18945Resumé
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 formal
system; 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 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. 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 believe
is the primary technical problem: expressiveness and feasibility for checking of formal systems and representations of mathematical notions.
Downloads
Publiceret
1997-01-18
Citation/Eksport
Pollack, R. (1997). How to Believe a Machine-Checked Proof. BRICS Report Series, 4(18). https://doi.org/10.7146/brics.v4i18.18945
Nummer
Sektion
Artikler
Licens
Authors who publish with this journal agree to the following terms:- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).