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