A departure from my usual topics, in remembrance of my college math classes (and with a nod to Mozilla folks working on related areas like automated testing and software verification): Via Eric Drexler via Emergent Chaos comes this interesting review paper on formal proofs in mathematics and software to verify them.
As a dual math/physics major I was well acquainted with jokes about the lack of mathematical rigor on the part of physicists, who often engaged in rather slapdash simplifications in their drive to get formulas they could use to explain experimental data and make further predictions. However physicists who cut corners are ultimately saved by the fact that nature will check their work and let them know if they’ve made bonehead mistakes.
On the other hand mathematicians traditionally have had only other mathematicians to save them from errors, and most mathematicians find it more personally and professionally rewarding to do their own original work instead of verifying that of others. Enter computers, which are happy to do such relatively mindless tasks. Of course the catch is that you have to instruct them in how to do this, and like conventional programming this requires specifying the task at hand in excruciating detail, including all the steps that mathematicians leave out in conventional proofs (marked by phrases like “we can clearly see that . . .“).
Read the paper for how this is done; it’s pretty comprehensible even if (like me) you’ve forgotten almost all your college math. My favorite bit of the paper (speaking of the HOL Light theorem prover):
All the basic theorems of mathematics up through the Fundamental Theorem of Calculus are proved from scratch on the user’s laptop in about two minutes every time the system loads, so that the casual user does not need to be concerned with the low-level details.
In other words, it’s booting mathematics! And like conventional booting, people still get impatient; the HOL LIght tutorial describes how to cheat and checkpoint the system so you can skip the boring stuff.
I was also enchanted by the fact that multiple theorem provers have been developed, and mathematicians in different countries have their own favorite systems. Thus they replicate in cyberspace the traditional national styles (English, French, German, Hungarian, etc.) of mathematics. However it turns out that this is actually useful and not wasted work, as the different theorem provers can check each others’ efforts and thus increase confidence in their underlying correctness.
Finally, a lot of these systems are released as free and open source software, so if you want to try your hand at formalizing some famous theorems everything you need is just a download away.
John Nash (nobody@devnull.spamcop.net) - 2008-12-11 06:01
Hey Fermat’s last Theorem is up for grabs
hyperdanja » Blog Archive » links for 2008-12-11 - 2008-12-12 00:04
[…] Machine-verified formal mathematical proofs « Frank Hecker “All the basic theorems of mathematics up through the Fundamental Theorem of Calculus are proved from scratch on the user’s laptop in about two minutes every time the system loads, so that the casual user does not need to be concerned with the low-level details.” (tags: proof maths) […]
Flug - 2009-01-20 12:32
I was surprised by the bunch of programs that exist to prove theorems. I am looking forward to play around a with them, since I am really exicted and curious about the outcomes. Thanks for sharing!