# 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 www.ams.org/notices .

Source: American Mathematical Society

## Related Stories

#### More evidence for ninth planet roaming solar system's outer fringes

October 19, 2016

As the search for a hypothetical, unseen planet far, far beyond Neptune's orbit continues, research by a team of the University of Arizona provides additional support for the possible existence of such a world and narrows ...

#### On Philippine isle, research pinpoints 'bull's-eye' of biodiversity

October 17, 2016

Colonial plunder, crime, tribal factions, sectarianism, drug running, piracy, animal poaching, illegal logging and destructive mining practices—all of which add up to wholesale environmental exploitation. The island of ...

#### How vulnerable to hacking is the US election cyber infrastructure?

August 1, 2016

Following the hack of Democratic National Committee emails and reports of a new cyberattack against the Democratic Congressional Campaign Committee, worries abound that foreign nations may be clandestinely involved in the ...

#### Team announces construction of a formal computer-verified proof of the Kepler conjecture

August 13, 2014

(Phys.org) —A team of researchers led by the man, Thomas Hales, who came up with written proof of the Kepler conjecture is now reporting that they have constructed a formal proof of the conjecture, which implies the use ...

#### Six-year journey leads to proof of Feit-Thompson Theorem

October 12, 2012

At 5:46 p.m. on Sept. 20, Georges Gonthier, principal researcher at Microsoft Research Cambridge, sent a brief email to his colleagues at the Microsoft Research-Inria Joint Centre in Paris. It read, in full: "This is really ...

#### NPR's 'Math Guy' explains changing nature of mathematical proof

February 20, 2006

Keith Devlin is a consulting professor in Stanford's Mathematics Department and a fellow of the American Association for the Advancement of Science. Some biologists recognize his name because there's an extinct possum named ...

## Recommended for you

#### Ancient parrot fossil found in Siberia

October 26, 2016

(Phys.org)—A Russian paleontologist has discovered a parrot fossil uncovered in Siberia several years ago—the first evidence of parrots living in Asia. In his paper published in Biology Letters, Nikita Zelenkov describes ...

#### Ancient burials suggestive of blood feuds

October 24, 2016

There is significant variation in how different cultures over time have dealt with the dead. Yet, at a very basic level, funerals in the Sonoran Desert thousands of years ago were similar to what they are today. Bodies of ...

#### Dinosaurs of a feather flock and die together?

October 24, 2016

In the paleontology popularity contest, studying the social life of dinosaurs is on the rise.

#### Model helps explore how changing certainty in belief of one statement can lead to changings belief in truth of others

October 21, 2016

A small team of researchers with members from the U.S., the Netherlands, Russia and Italy has developed a new model that illuminates how changing the degree of certainty a person holds for a given belief can lead to changes ...

#### Science sheds light on 250-year-old literary controversy

October 21, 2016

The social networks behind one of the most famous literary controversies of all time have been uncovered using modern networks science.

#### Meet Savannasaurus, Australia's newest titanosaur

October 21, 2016

The outback region around Winton in central Queensland is arguably Australia's ground zero for giant dinosaur fossils. Here, graziers occasionally stumble across petrified bones on their paddocks, amid the stubbly grass and ...