A mathematical proof is a manifestation of pure logic and truth. But an increasing number of mathematical proofs are now impossible to verify with absolute certainty, safe through the latest development of computer tools.
When mathematicians prove theorems traditionally, they usually present the argument in narrative form. They gloss over details they think other experts will understand; they take shortcuts to make the presentation less tedious, they appeal to intuition, etc. The correctness of the arguments is subject to the scrutiny of other mathematicians. It is sobering to realize that the means by which mathematical results are verified is essentially a social process and is thus fallible. When it comes to central, well-known results, the proofs are exceptionally checked, and errors eventually found.
Nevertheless, there are many undetected false results in mathematical history, as other require complicated proofs. To get around these problems, computer scientists and mathematicians began to develop the field of formal proof powerful enough to handle difficult proofs.
In simple cases, one can feed a statement to a computer proof assistant and expect it to hand over a proof. Rather, the mathematician has to know how to prove the statement; the proof then is greatly expanded into the special syntax of formal proof with well spelled out steps. Computers can also explore mathematics on their own, coming up with unnoticed exciting conjectures.
Four new articles explore the current state of the art of formal proof and provide practical guidance for using computer proof assistants. One long-term dream is to have formal proofs of all of the central theorems in mathematics, and the four collections of proof would be akin to “the sequencing of the mathematical genome.”