A ground-breaking collection of four articles by leading experts, published today in the Notices of the American Mathematical Society (and freely available), explores new developments in the use of formal proof 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.”

New computer tools have the potential to revolutionize the practice of mathematics by providing far more-reliable proofs of mathematical results than have ever been possible in the history of humankind. These computer tools, based on the notion of “formal proof,” have in recent years been used to provide nearly infallible proofs of many important results in mathematics.