Yes, I think there is a striking difference between how
mathematicians think about proofs in practice and the widespread
assumption that they can "in principle" be formalized in set
theory. The following talk I gave a while ago talks a bit about
this distinction, among other things.
http://www.cl.cam.ac.uk/~jrh13/slides/principia-27nov10/slides.pdf
John, that looks like a great article!
Mathematical proofs are subjected to peer review, but errors often
escape unnoticed.
Here's one relevant example. Birkhoff in the top US journal (Annals
of Math) gave his own rigorous axioms for Euclidean Geometry, never
mentioning Hilbert's work 30 years earlier. He had one axiom that
requires a function taking values in R/ 2pi to be continuous. He only
used it to show that all 3 angles in a triangle are either clockwise
or counterclockwise. He publised an erratum for that proof, which I
can't read. MacLane wrote up 20 years late a rigorous version of
Birkhoff's proof, and I think I simplified MacLane's proof, taking out
the continuous functions, which no Geometry student could understand.
Arguably, HOL Light is the computer-age version of Principia:
. The logical basis is simple type theory, which was distilled
(Ramsey, Chwistek, Church) from PM’s original logic.
. Everything, even arithmetic on numbers, is done from first
principles by reduction to the primitive logical basis.
This is really cool, and I'd like to understand it. It must be
discussed in reference.pdf. I never got the point of Principia, but
I'd like to, and Greenberg's book has a great quote from Russell:
MG> The value of Euclid's work as a masterpiece of logic has been
MG> very grossly exaggerated.
Three notable recent formal proofs in pure mathematics:
. Prime Number Theorem — Jeremy Avigad et al (Isabelle/HOL),
John Harrison (HOL Light)
Cool! Jeremy was posting on the Isabelle group about his 69 page
paper giving a rigorization of Euclid quite different from Hilbert &
Tarski: not fixing the axioms, but formalizing Euclid's diagrams.
Some successes for verification using theorem proving technology:
• Microcode algorithms for floating-point division, square root and
several transcendental functions on Intel® Itanium® processor
family (John Harrison, HOL Light)
I'd like to know more about your success here. You must have written
papers about this for Intel folks. Probably most of what you do is
too technical for me to follow, but I'd really like to understand the
connection between theorems, floating point algorithms, and HOL Light.
After a full four years of deliberation, [Hales's] reviewers returned:
“The news from the referees is bad, from my perspective.
They have not been able to certify the correctness of the
proof, and will not be able to certify it in the future, because
they have run out of energy to devote to the problem. This is
not what I had hoped for.
Hah! Tom put a much better spin in his Notices article about the
Annals referees.
Hales’s proof was eventually published, and no significant error
has been found in it. Nevertheless, the verdict is disappointingly
lacking in clarity and finality.
I've got a better spin: that's why Tom is working so hard on proof
assistants to formalize his proof. If Tom had gotten full credit for
solving the Kepler conjecture, he'd be resting on his laurels!
Indeed, I see formal methods as fundamental to the long-term growth
of mathematics. (Hales, The Kepler Conjecture)
Uh, maybe I was wrong. But still, the credit Tom didn't get is a
powerful goad to keep him working on formal methods.
Anyway, that was modest of you to not point out that you (and Nipkow
the Isabelle author!) are a coauthor of Tom's:
Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias;
Obua, Steven; Zumkeller, Roland A revision of the proof of the Kepler
conjecture. Discrete Comput. Geom. 44 (2010), no. 1, 1–34.
--
Best,
Bill
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
