State of Theorem Proving Systems 2008

By Xah Lee. Date:

Recently American Mathematical Society published a series of articles on formal proofs. See: There are 4 articles:

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,” …

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.
YearTheoremProof SystemFormalizerTraditional Proof
1986First IncompletenessBoyer-MooreShankarGödel
1990Quadratic ReciprocityBoyer-MooreRussinoffEisenstein
1996Fundamental - of CalculusHOL LightHarrisonHenstock
2000Fundamental - of AlgebraMizarMilewskiBrynski
2000Fundamental - of AlgebraCoqGeuvers et al.Kneser
2004Four-ColorCoqGonthierRobertson et al.
2004Prime NumberIsabelleAvigad et al.Selberg-Erdös
2005Jordan CurveHOL LightHalesThomassen
2005Brouwer FixedPoint HOL LightHarrisonKuhn
2006Flyspeck IIsabelleBauer-NipkowHales
2007Cauchy ResidueHOL LightHarrisonclassical
2008Prime NumberHOL LightHarrisonanalytic 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 AssistantProof Style
HOL Lightprocedural
Isabelleboth possible

In mathematics there have been three main revolutions:

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.