The four Notices articles explore the current state of the art of formal proof and provide practical guidance for using computer proof assistants.  If the use of these assistants becomes widespread, they could change deeply mathematics as it is currently practiced.  One long-term dream is to have formal proofs of all of the central theorems in mathematics.  Thomas Hales, one of the authors writing in the Notices, says that such a collection of proofs would be akin to "the sequencing of the mathematical genome".

The four articles are:

Formal Proof, by Thomas Hales, University of Pittsburgh

Formal Proof---Theory and Practice, by John Harrison, Intel Corporation

Formal proof---The Four Colour Theorem, by Georges Gonthier, Microsoft   Research, Cambridge, England

Formal Proof---Getting Started, by Freek Wiedijk, Radboud University,   Nijmegen, Netherlands

The articles appear today in the December 2008 issue of the Notices and are freely available without a subscription.