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

##### Nov 06, 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

#### What if our children are the screen-obsessed couch potatoes of the future?

Mar 30, 2015

The idea of "digital addiction" has returned to the fore with UCL researchers suggesting physical activity should displace the compulsive watching of television, internet surfing and video gaming. Often it ...

#### Governments want to regulate bitcoin – is that even possible?

Mar 26, 2015

The UK government has shown its intention to regulate bitcoin and other digital currencies, drawing them into the realms of financial regulation applied to banks and other financial services. But bitcoin ...

#### Zoo innovations has animals foraging for food

Mar 20, 2015

When red pandas go on exhibit for the first time at Brookfield Zoo in July, they'll be housed around a broad tree that looks like a giant bonsai and has magical qualities.

#### Conifers' helicoptering seeds are result of long evolutionary experiment

Mar 17, 2015

The whirling, winged seeds of today's conifers are an engineering wonder and, as University of California, Berkeley, scientists show, a result of about 270 million years of evolution by trees experimenting ...

#### MH370 report: Underwater locator beacon battery had expired

Mar 08, 2015

The first comprehensive report into the disappearance of Malaysia Airlines Flight 370 revealed Sunday that the battery of the locator beacon for the plane's data recorder had expired more than a year before ...

#### Researchers confirm that neonicotinoid insecticides impair bee's brains

Feb 05, 2015

Research at the Universities of St Andrews and Dundee has confirmed that levels of neonicotinoid insecticides accepted to exist in agriculture cause both impairment of bumblebees' brain cells and subsequent ...

## Recommended for you

#### Immigration appeals process lacks consistency, fairness, research shows

18 minutes ago

The federal immigration appeals process lacks consistency because it reviews a small and skewed sample of cases, according to new Stanford research.

#### The Rice Crisis: Tracking an asset-price bubble in the check-out line

32 minutes ago

Princeton economist Harrison Hong has spent much of his career working to understand how and why asset-price bubbles form. Hong, the John H. Scully '66 Professor in Finance, has studied the dot-com bubble ...

#### Colorblind bilingual programs can perpetuate bias, study finds

43 minutes ago

Many presume bilingual education can level the academic playing field for English learners, but one UC Davis professor calls foul on current practices.

#### Signs of climate change and adaptation in the ancient Maya lowlands

1 hour ago

A new study pinpoints the devastating effects of climate change on ancient Maya civilization, despite attempts to adapt to it.

#### Expert offers advice on how to 'pitch' a good research idea

15 hours ago

For many students or junior academics—and even for senior investigators—initiating a new piece of research can be a daunting experience, and they often do not know where or how to begin. A recent Accounting and Finance ar ...

#### A better grasp of primate grip

15 hours ago

Scientists are coming to grips with the superior grasping ability of humans and other primates throughout history.