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

Explore further: Researchers help Boston Marathon organizers plan for 2014 race

Related Stories

If you want to trust a robot, look at how it makes decisions

Mar 11, 2014

Robots, and autonomous systems in general, can cause anxiety and uncertainty, particularly as their use in everyday tasks becomes a more immediate possibility. In order to lessen at least some of that anxiety, ...

Platform would protect smartphones from cyber criminals

Mar 06, 2014

Criminals don't have to pick your pocket to get what they want out of your mobile. But a certifiably secure operating platform is being developed by Swedish researchers so that consumers can be confident that their mobile ...

Build it and they will believe, says defiant China tycoon

Jan 16, 2014

A Chinese multi-millionaire who built himself an Egyptian pyramid and a replica of Versailles vows to construct the world's tallest building in just six months—despite authorities preventing work amid safety ...

The app that checks whether your date is a sex offender

Jan 14, 2014

An app on offer in the US says it can determine whether the person you are dating has anything to hide, using facial recognition to see if they are on the sex offenders register. ...

Facebook data funneled to Russian search engine Yandex

Jan 14, 2014

Yandex on Tuesday announced that it is adding public Facebook data to the index of data mined for queries handled by the Russian Internet search giant.

Indonesia struggles to clean up corrupt forestry sector

Jan 01, 2014

Deep in the forests of Borneo island, workmen from an Indonesian timber company fell a tree with a chainsaw, stick a red tag with a serial number onto it and attach a corresponding stub to the stump.

Recommended for you

Egypt archaeologists find ancient writer's tomb

1 hour ago

Egypt's minister of antiquities says a team of Spanish archaeologists has discovered two tombs in the southern part of the country, one of them belonging to a writer and containing a trove of artifacts including reed pens ...

Researchers create methylation maps of Neanderthals and Denisovans, compare them to modern humans

Apr 18, 2014

(Phys.org) —A team of Israeli, Spanish and German researchers has for the first time created a map of gene expression in Neanderthals and Denisovans and has compared them with modern humans. In their paper ...

3 Qs: Economist makes the case for new quasi-experiments as a way of studying environmental issues

Apr 18, 2014

How can scholars get traction on environmental problems, particularly those relating to pollution? In an essay appearing in this week's issue of the journal Science, MIT economist Michael Greenstone, along ...

New specimens of Yanornis indicate a digestive system of living birds

Apr 18, 2014

In a recent paper describing ten new specimens of Yanornis martini identified by the director of the Shandong Tianyu Museum of Natural History Mr. Xiaoting Zheng, an international team of scientists lead ...

Study finds law dramatically curbing need for speed

Apr 18, 2014

Almost seven years have passed since Ontario's street-racing legislation hit the books and, according to one Western researcher, it has succeeded in putting the brakes on the number of convictions and, more importantly, injuries ...

Changing dinosaur tracks spurs novel approach

Apr 17, 2014

Paleontologists are using a range of old and new techniques to map the Broome Sandstone dinosaur trackways.

Icester
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!)

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

More news stories

Egypt archaeologists find ancient writer's tomb

Egypt's minister of antiquities says a team of Spanish archaeologists has discovered two tombs in the southern part of the country, one of them belonging to a writer and containing a trove of artifacts including reed pens ...

Researchers create methylation maps of Neanderthals and Denisovans, compare them to modern humans

(Phys.org) —A team of Israeli, Spanish and German researchers has for the first time created a map of gene expression in Neanderthals and Denisovans and has compared them with modern humans. In their paper ...

Last Week's Best—Quantum mechanics breakthrough, 3-D printed human heart, and paraplegia therapy

(Phys.org) —Hello readers—we'd like to try something new here at Phys.org and Medical Xpress: offer a weekly summary every Monday highlighting what we feel are the most important stories of the past ...

Earliest ancestor of land herbivores discovered

New research from the University of Toronto Mississauga demonstrates how carnivores transitioned into herbivores for the first time on land.

Neanderthals and Cro-magnons did not coincide on the Iberian Peninsula

The meeting between a Neanderthal and one of the first humans, which we used to picture in our minds, did not happen on the Iberian Peninsula. That is the conclusion reached by an international team of researchers ...

NASA's space station Robonaut finally getting legs

Robonaut, the first out-of-this-world humanoid, is finally getting its space legs. For three years, Robonaut has had to manage from the waist up. This new pair of legs means the experimental robot—now stuck ...

Ex-Apple chief plans mobile phone for India

Former Apple chief executive John Sculley, whose marketing skills helped bring the personal computer to desktops worldwide, says he plans to launch a mobile phone in India to exploit its still largely untapped ...

Filipino tests negative for Middle East virus

A Filipino nurse who tested positive for the Middle East virus has been found free of infection in a subsequent examination after he returned home, Philippine health officials said Saturday.

Free the seed: OSSI nurtures growing plants without patent barriers

(Phys.org) —Members of the Open Source Seed Initiative this week held a rally and seed giveaway event. The group is concerned over restricting access to seeds through patents. They are stirring up public ...