Abstract: Using computers in proofs both extends mathematics with new results and creates new mathematical questions about the nature and technique of such proofs. This special issue features a collection of articles by practioners and theorists of such formal proofs which explore both aspects.

TOC:

   - Formal Proof by Thomas C. Hales
   - Formal Proof—The Four-Color Theorem by Georges Gonthier
   - Formal Proof—Theory and Practice by John Harrison
   - Formal Proof—Getting Started by Freek Wiedijk

[pdf]