State of Theorem Proving Systems 2008
Recently American Mathematical Society published a series of articles on formal proofs. See: http://www.ams.org/notices/200811/. There are 4 articles:
- Formal Proof by Thomas Hales
- Formal Proof — The Four-Color Theorem by Georges Gonthier
- Formal Proof — Theory and Practice by John Harrison
- Formal Proof — Getting Started by Freek Wiedijk
Here's some excerpt from Formal Proof by Thomas Hales that stands out for me.
Quite often, lip service is paid to formal logical foundations: “…the correctness of a mathematical text is verified by comparing it, more or less explicitly, with the rules of a formalized language. [4] A mathematical proof is rigorous when it is (or could be) written out in the first-order predicate language L(∈) as a sequence of inferences from the axioms ZFC, each inference made according to one of the stated rules. [19]”
Yet mathematicians seldom make set-theoretic axioms explicit in their work, except for those whose results depend on more “exotic” hypotheses. And there is little use of formal proof, or even formal logical notation, in everyday mathematics; Dijkstra has remarked that “as far as the mathematical community is concerned George Boole has lived in vain”.
…
Russell in his autobiography remarks that his intellect “never quite recovered from the strain” of writing Principia Mathematica, and as Bourbaki [4] notes: “If formalized mathematics were as simple as the game of chess, then once our chosen formalized language had been described there would remain only the task of writing out our proofs in this language, […] But the matter is far from being as simple as that, and no great experience is necessary to perceive that such a project is absolutely unrealizable: the tiniest proof at the beginning of the Theory of Sets would already require several hundreds of signs for its complete formalization. […] formalized mathematics cannot in practice be written down in full, […] We shall therefore very quickly abandon formalized mathematics, […]”
…
Like Nidditch, who complained that “in the whole literature of mathematics there is not a single valid proof in the logical sense,” …
- [4] Theory of sets: Elements of mathematics By N Bourbaki. Buy at amazon
- [19] Mathematics: Form and Function By S Mac Lane. Buy at amazon
The following are quotes from Formal Proof , by Thomas C Hales.
There is a wide gulf that separates traditional proof from formal proof. For example, Bourbaki's Theory of Sets was designed as a purely theoretical edifice that was never intended to be used in the proof of actual theorems. Indeed, Bourbaki declares that “formalized mathematics cannot in practice be written down in full” and calls such a project “absolutely unrealizable”.
Table 1. Examples of formal proofs. Year Theorem Proof System Formalizer Traditional Proof 1986 First Incompleteness Boyer-Moore Shankar Gödel 1990 Quadratic Reciprocity Boyer-Moore Russinoff Eisenstein 1996 Fundamental - of Calculus HOL Light Harrison Henstock 2000 Fundamental - of Algebra Mizar Milewski Brynski 2000 Fundamental - of Algebra Coq Geuvers et al. Kneser 2004 Four-Color Coq Gonthier Robertson et al. 2004 Prime Number Isabelle Avigad et al. Selberg-Erdös 2005 Jordan Curve HOL Light Hales Thomassen 2005 Brouwer Fixed Point HOL Light Harrison Kuhn 2006 Flyspeck I Isabelle Bauer-Nipkow Hales 2007 Cauchy Residue HOL Light Harrison classical 2008 Prime Number HOL Light Harrison analytic proof The transcription of a single traditional proof into a formal proof is a major undertaking.
Computer proof assistants have been under development for decades (see Box “Early Milestones”), but only recently has it become a practical matter to prove major theorems formally. The most spectacular example is Gonthier's formal proof of the four-color theorem. His starting point is the second-generation proof by Robertson et al. Although the traditional proof uses a computer and Gonthier uses a computer, the two computer processes differ from one another in the same way that a traditional proof differs from a formal proof. They differ in the same way that adding 1 + 1 = 2 on a calculator differs from the mathematical justification of 1 + 1 = 2 by definitions, recursion, and a rigorous construction of the natural numbers. In short, a large logical gulf separates them. As a result of Gonthier's formalization, the proof of the four-color theorem has become one of the most meticulously verified proofs in history.
There are several competing systems to choose from, built on various logical foundations, and with their own powerful features. People argue about the relative merits of the different systems much in the same way that people argue about the relative merits of operating systems, political loyalties, or programming languages. To some extent, preferences show a geographical bias: HOL in the UK, Mizar in Poland, Coq in France, and Isabelle in Germany and the UK.
Here's some intro of theorem proving systems.
LCF (Logic for Computable Functions) is the earlist system by Robin Milner et al in the 1970s. He also designed the functional language ML (OCaml, F# are derivatives of ML. (See also: OCaml Tutorial)).
From LCF, are derived a series of systems called HOL (Higher Order Logic). The current one is HOL Light. These are usually implemented in ML family of langs. HOL Light gave birth to Isabelle.
Apart from the above lineage, there's Mizar system, which began in 1973. It is a commercial system, written in Pascal. It has its own active professional community and active journal. Seems to have the largest established base.
Another major one is Coq. Developed in France.
Suggested book from the above article: Mechanizing Proof: Computing, Risk, and Trust , by Donald A MacKenzie. Buy at amazon
Formal Proof: Getting Started , by Freek Wiedijk, excerpts:
Proof Assistant Proof Style HOL Light procedural Mizar declarative ProofPower procedural Isabelle both possible Coq procedural In mathematics there have been three main revolutions:
- The introduction of proof by the Greeks in the fourth century BC, culminating in Euclid'sElements.
- The introduction of rigor in mathematics in the nineteenth century. During this time the non rigorous calculus was made rigorous by Cauchy and others. This time also saw the development of mathematical logic by Frege and the development of set theory by Cantor.
- The introduction of formal mathematics in the late twentieth and early twenty-first centuries.
Most mathematicians are not aware that this third revolution already has happened, and many probably will disagree that this revolution even is needed. However, in a few centuries mathematicians will look back at our time as the time of this revolution. In that future most mathematicians will not consider mathematics to be definitive unless it has been fully formalized.