Featured Research

from universities, journals, and other organizations

Computers Effective In Verifying Mathematical Proofs

Date:
November 7, 2008
Source:
American Mathematical Society
Summary:
New computer tools have the potential to revolutionize the practice of mathematics by providing more-reliable proofs of mathematical results than have ever been possible in the history of humankind. These tools, based on the notion of "formal proof," have in recent years been used to provide nearly infallible proofs of many important results.

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.

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.

Four new articles in the December 2008 issue of Notices of the American Mathematical Society 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:

  1. Formal Proof, by Thomas Hales, University of Pittsburgh
  2. Formal Proof---Theory and Practice, by John Harrison, Intel Corporation
  3. Formal proof---The Four Colour Theorem, by Georges Gonthier, Microsoft Research, Cambridge, England
  4. Formal Proof---Getting Started, by Freek Wiedijk, Radboud University, Nijmegen, Netherlands

Story Source:

The above story is based on materials provided by American Mathematical Society. Note: Materials may be edited for content and length.


Cite This Page:

American Mathematical Society. "Computers Effective In Verifying Mathematical Proofs." ScienceDaily. ScienceDaily, 7 November 2008. <www.sciencedaily.com/releases/2008/11/081106153638.htm>.
American Mathematical Society. (2008, November 7). Computers Effective In Verifying Mathematical Proofs. ScienceDaily. Retrieved October 23, 2014 from www.sciencedaily.com/releases/2008/11/081106153638.htm
American Mathematical Society. "Computers Effective In Verifying Mathematical Proofs." ScienceDaily. www.sciencedaily.com/releases/2008/11/081106153638.htm (accessed October 23, 2014).

Share This



More Computers & Math News

Thursday, October 23, 2014

Featured Research

from universities, journals, and other organizations


Featured Videos

from AP, Reuters, AFP, and other news services

Chameleon Camouflage to Give Tanks Cloaking Capabilities

Chameleon Camouflage to Give Tanks Cloaking Capabilities

Reuters - Innovations Video Online (Oct. 22, 2014) — Inspired by the way a chameleon changes its colour to disguise itself; scientists in Poland want to replace traditional camouflage paint with thousands of electrochromic plates that will continuously change colour to blend with its surroundings. The first PL-01 concept tank prototype will be tested within a few years, with scientists predicting that a similar technology could even be woven into the fabric of a soldiers' clothing making them virtually invisible to the naked eye. Matthew Stock reports. Video provided by Reuters
Powered by NewsLook.com
Internet of Things Aims to Smarten Your Life

Internet of Things Aims to Smarten Your Life

AP (Oct. 22, 2014) — As more and more Bluetooth-enabled devices are reaching consumers, developers are busy connecting them together as part of the Internet of Things. (Oct. 22) Video provided by AP
Powered by NewsLook.com
Free Math App Is A Teacher's Worst Nightmare

Free Math App Is A Teacher's Worst Nightmare

Newsy (Oct. 22, 2014) — New photo-recognition software from MicroBlink, called PhotoMath, solves linear equations and simple math problems with step-by-step results. Video provided by Newsy
Powered by NewsLook.com
Rate Hike Worries Down on Inflation Data

Rate Hike Worries Down on Inflation Data

Reuters - Business Video Online (Oct. 22, 2014) — Inflation remains well under control according to the latest consumer price index, giving the Federal Reserve more room to keep interest rates low for awhile. Bobbi Rebell reports. Video provided by Reuters
Powered by NewsLook.com

Search ScienceDaily

Number of stories in archives: 140,361

Find with keyword(s):
 
Enter a keyword or phrase to search ScienceDaily for related topics and research stories.

Save/Print:
Share:  

Breaking News:

Strange & Offbeat Stories

 

Space & Time

Matter & Energy

Computers & Math

In Other News

... from NewsDaily.com

Science News

Health News

Environment News

Technology News



Save/Print:
Share:  

Free Subscriptions


Get the latest science news with ScienceDaily's free email newsletters, updated daily and weekly. Or view hourly updated newsfeeds in your RSS reader:

Get Social & Mobile


Keep up to date with the latest news from ScienceDaily via social networks and mobile apps:

Have Feedback?


Tell us what you think of ScienceDaily -- we welcome both positive and negative comments. Have any problems using the site? Questions?
Mobile iPhone Android Web
Follow Facebook Twitter Google+
Subscribe RSS Feeds Email Newsletters
Latest Headlines Health & Medicine Mind & Brain Space & Time Matter & Energy Computers & Math Plants & Animals Earth & Climate Fossils & Ruins