Of interest.
recently American Mathematical Society published a series of articles
on formal proofs.
See:
http://www.ams.org/notices/200811/
the articles include:
Formal Proof
Thomas Hales
Formal Proof--The Four-Color Theorem
Georges Gonthier
Formal Proof--Theory and Practice
John Harrison
Formal Proof--Getting Started
Freek Wiedijk
they are freely downloadable in PDF.
-------------------------------------------
Also of interest, my own blog of old:
• The Codification of Mathematics
http://xahlee.org/cmaci/notation/math_codify.html
• The Concepts and Confusions of Prefix, Infix, Postfix and Fully
Nested Notations
http://xahlee.org/UnixResource_dir/writ/notations.html
Xah
∑ http://xahlee.org/
☄
i have just finished reading 3 articles on formal proofs published by
AMS.
I've wrote a short blog-style notes, mostly excerpts from the article
of points of interest to me. I thought it would be of interest to
functional programers here, esp most of you are unfamiliar in the
realm of math.
the blog is at the bottom of:
• The Codification of Mathematics
http://xahlee.org/cmaci/notation/math_codify.html
plain text excerpt follows. (lacks coloring and table formatting)
--------------------------------------------
Current State Of Theorem Proving Systems
2008-12-02
Recently American Mathematical Society published a series of articles
on formal proofs. See: http://www.ams.org/notices/200811/. the
articles include:
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 quotes in “Formal Proof by Thomas Hales” that stands out
from 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 writ- ing out our proofs
in this lan- guage, [...] 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 tini- est proof at the
beginning of the Theory of Sets would already re- quire 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] N. Bourbaki, Theory of sets, Elements of mathematics, 1968.
[19] S. Mac Lane, Mathematics: Form and Function, 1986.
»
----------------------
The following are quotes from “Formal Proof” (2008) 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.).
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” (2004) by Donald A. MacKenzie↗. (amazon.com↗)
“Formal Proof: Getting Started” (2008-12) 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.
»
Xah
∑ http://xahlee.org/
☄