Ars Mathematica

Scott Aaronson asks why mathematicians haven’t switched to machine-checkable proofs, and answers his own question by exhibiting the basically-human-unreadable proof of the irrationality of the square root of two using the HOL Light theorem prover. Scott provides a few interesting links:

• Adventures in the Verification of Mathematics, an essay discussing some of the issues by Harvey Friedman.
• Formalizing 100 Theorems, a list of a 100 candidate theorems for verification, and the systems that have verified them, by Freek Wiedijk.
• The Seventeen Provers of the World, a book-length comparison of different formalizations of the proof of the irrationality of the square root of 2, also by Freek Wiedijk

There is also the Flyspeck Project, a project to formalize Thomas Hales’ computer proof of the Kepler conjecture, which we mentioned once before.