Forum for Science, Industry and Business

Sponsored by:     3M 
Search our Site:


Proof by Computer

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 SocietyNotices 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
Founded in 1888 to further mathematical research and scholarship, today the American Mathematical Society has more than 32,000 members. The Society fulfills its mission through programs and services that promote mathematical research and its uses, strengthen mathematical education, and foster awareness and appreciation of mathematics and its connections to other disciplines and to everyday life.

Prof. Thomas Hales | Newswise Science News
Further information:

More articles from Information Technology:

nachricht Fraunhofer FIT joins Facebook's Telecom Infra Project
25.10.2016 | Fraunhofer-Institut für Angewandte Informationstechnik FIT

nachricht Stanford researchers create new special-purpose computer that may someday save us billions
21.10.2016 | Stanford University

All articles from Information Technology >>>

The most recent press releases about innovation >>>

Die letzten 5 Focus-News des innovations-reports im Überblick:

Im Focus: Etching Microstructures with Lasers

Ultrafast lasers have introduced new possibilities in engraving ultrafine structures, and scientists are now also investigating how to use them to etch microstructures into thin glass. There are possible applications in analytics (lab on a chip) and especially in electronics and the consumer sector, where great interest has been shown.

This new method was born of a surprising phenomenon: irradiating glass in a particular way with an ultrafast laser has the effect of making the glass up to a...

Im Focus: Light-driven atomic rotations excite magnetic waves

Terahertz excitation of selected crystal vibrations leads to an effective magnetic field that drives coherent spin motion

Controlling functional properties by light is one of the grand goals in modern condensed matter physics and materials science. A new study now demonstrates how...

Im Focus: New 3-D wiring technique brings scalable quantum computers closer to reality

Researchers from the Institute for Quantum Computing (IQC) at the University of Waterloo led the development of a new extensible wiring technique capable of controlling superconducting quantum bits, representing a significant step towards to the realization of a scalable quantum computer.

"The quantum socket is a wiring method that uses three-dimensional wires based on spring-loaded pins to address individual qubits," said Jeremy Béjanin, a PhD...

Im Focus: Scientists develop a semiconductor nanocomposite material that moves in response to light

In a paper in Scientific Reports, a research team at Worcester Polytechnic Institute describes a novel light-activated phenomenon that could become the basis for applications as diverse as microscopic robotic grippers and more efficient solar cells.

A research team at Worcester Polytechnic Institute (WPI) has developed a revolutionary, light-activated semiconductor nanocomposite material that can be used...

Im Focus: Diamonds aren't forever: Sandia, Harvard team create first quantum computer bridge

By forcefully embedding two silicon atoms in a diamond matrix, Sandia researchers have demonstrated for the first time on a single chip all the components needed to create a quantum bridge to link quantum computers together.

"People have already built small quantum computers," says Sandia researcher Ryan Camacho. "Maybe the first useful one won't be a single giant quantum computer...

All Focus news of the innovation-report >>>



Event News

#IC2S2: When Social Science meets Computer Science - GESIS will host the IC2S2 conference 2017

14.10.2016 | Event News

Agricultural Trade Developments and Potentials in Central Asia and the South Caucasus

14.10.2016 | Event News

World Health Summit – Day Three: A Call to Action

12.10.2016 | Event News

Latest News

How nanoscience will improve our health and lives in the coming years

27.10.2016 | Materials Sciences

OU-led team discovers rare, newborn tri-star system using ALMA

27.10.2016 | Physics and Astronomy

'Neighbor maps' reveal the genome's 3-D shape

27.10.2016 | Life Sciences

More VideoLinks >>>