Proof by computer: Harnessing the power of computers to verify mathematical proofs

November 6, 2008

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

When mathematicians prove theorems in the traditional way, they present the argument in narrative form. They assume previous results, 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 determined by the scrutiny of other mathematicians, in informal discussions, in lectures, or in journals. 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 especially well checked and errors are eventually found. Nevertheless the history of mathematics has many stories about false results that went undetected for a long time.

In addition, in some recent cases, important theorems have required such long and complicated proofs that very few people have the time, energy, and necessary background to check through them. And some proofs contain extensive computer code to, for example, check a lot of cases that would be infeasible to check by hand. How can mathematicians be sure that such proofs are reliable?

To get around these problems, computer scientists and mathematicians began to develop the field of formal proof. A formal proof is one in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. Mathematicians do not usually write formal proofs because such proofs are so long and cumbersome that it would be impossible to have them checked by human mathematicians. But now one can get "computer proof assistants" to do the checking. In recent years, computer proof assistants have become powerful enough to handle difficult proofs.

Only in simple cases can one 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 every step spelled out, and it is this formal proof that the computer checks. It is also possible to let computers loose to explore mathematics on their own, and in some cases they have come up with interesting conjectures that went unnoticed by mathematicians. We may be close to seeing how computers, rather than humans, would do mathematics.

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 at .

Source: American Mathematical Society

Explore further: ELaNa XIV CubeSats launch on JPSS-1 mission

Related Stories

ELaNa XIV CubeSats launch on JPSS-1 mission

November 20, 2017

NASA has launched four small research satellites, or CubeSats, developed by four universities as part of a broader mission launching the next generation polar-orbiting satellite to space. These CubeSat missions were selected ...

First genetic proof that women were Viking warriors

September 8, 2017

New DNA evidence uncovered by researchers at Uppsala University and Stockholm University shows that there were in fact female Viking warriors. The remains of an iconic Swedish Viking Age grave now reveal that war was not ...

Improving web security without sacrificing performance

September 7, 2017

Chances are, you're reading this article on a web browser that uses HTTPS, the protocol over which data is sent between a web browser and the website users are connected to. In fact, nearly half of all web traffic passes ...

Recommended for you

How to cut your lawn for grasshoppers

November 22, 2017

Picture a grasshopper landing randomly on a lawn of fixed area. If it then jumps a certain distance in a random direction, what shape should the lawn be to maximise the chance that the grasshopper stays on the lawn after ...

Plague likely a Stone Age arrival to central Europe

November 22, 2017

A team of researchers led by scientists at the Max Planck Institute for the Science of Human History has sequenced the first six European genomes of the plague-causing bacterium Yersinia pestis dating from the Late Neolithic ...

Ancient barley took high road to China

November 21, 2017

First domesticated 10,000 years ago in the Fertile Crescent of the Middle East, wheat and barley took vastly different routes to China, with barley switching from a winter to both a winter and summer crop during a thousand-year ...


Adjust slider to filter visible comments by rank

Display comments: newest first

5 / 5 (1) Nov 06, 2008
Oh, thank goodness! Hopefully TI will release a calculator (TI-109?) that has a 'solve proof' function that provides blackboard answers like the TI-89/92 does for integrands and differentials! (just kidding, but, hey, it would be nice!)

not rated yet Nov 07, 2008
They will always keep assuming that 1 plus 1 = 2, while Bose-Einstein condensates make one wonder if that assumption is an illusion.

Please sign in to add a comment. Registration is free, and takes less than a minute. Read more

Click here to reset your password.
Sign in to get notified via email when new comments are made.