Using computers in proofs both extends mathematics with new results and creates new mathematical questions about the nature and technique of such proofs. The special issue of Notices of the American Mathematical Society features a collection of articles by practitioners and theories of such formal proofs which explore both aspects.
- Formal Proof by Thomas Hales
- Form Proof -- The Four-Color Theorem by Georges Gonthier
- Formal Proof -- Theory and Practice by John Harrison
- Fromal Proof -- Getting Started Freek Wiedijk