How to Believe a Machine-Checked Proof
AbstractSuppose 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? 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.
How to Cite
Pollack, R. (1997). How to Believe a Machine-Checked Proof. BRICS Report Series, 4(18). https://doi.org/10.7146/brics.v4i18.18945
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.