10.11.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 SocietyNotices of the American Mathematical Society (http://www.ams.org/notices), 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, MicrosoftResearch, 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 http://www.ams.org/notices.

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:

http://www.ams.org/notices

http://www.ams.org

**Further reports about:**
> Proof by Computer
> computer tools
> formal proof
> mathematical genome
> mathematics

Reversing cause and effect is no trouble for quantum computers

20.07.2018 | Centre for Quantum Technologies at the National University of Singapore

Study suggests buried Internet infrastructure at risk as sea levels rise

18.07.2018 | University of Wisconsin-Madison

A new manufacturing technique uses a process similar to newspaper printing to form smoother and more flexible metals for making ultrafast electronic devices.

The low-cost process, developed by Purdue University researchers, combines tools already used in industry for manufacturing metals on a large scale, but uses...

For the first time ever, scientists have determined the cosmic origin of highest-energy neutrinos. A research group led by IceCube scientist Elisa Resconi, spokesperson of the Collaborative Research Center SFB1258 at the Technical University of Munich (TUM), provides an important piece of evidence that the particles detected by the IceCube neutrino telescope at the South Pole originate from a galaxy four billion light-years away from Earth.

To rule out other origins with certainty, the team led by neutrino physicist Elisa Resconi from the Technical University of Munich and multi-wavelength...

For the first time a team of researchers have discovered two different phases of magnetic skyrmions in a single material. Physicists of the Technical Universities of Munich and Dresden and the University of Cologne can now better study and understand the properties of these magnetic structures, which are important for both basic research and applications.

Whirlpools are an everyday experience in a bath tub: When the water is drained a circular vortex is formed. Typically, such whirls are rather stable. Similar...

Physicists working with Roland Wester at the University of Innsbruck have investigated if and how chemical reactions can be influenced by targeted vibrational excitation of the reactants. They were able to demonstrate that excitation with a laser beam does not affect the efficiency of a chemical exchange reaction and that the excited molecular group acts only as a spectator in the reaction.

A frequently used reaction in organic chemistry is nucleophilic substitution. It plays, for example, an important role in in the synthesis of new chemical...

Optical spectroscopy allows investigating the energy structure and dynamic properties of complex quantum systems. Researchers from the University of Würzburg present two new approaches of coherent two-dimensional spectroscopy.

"Put an excitation into the system and observe how it evolves." According to physicist Professor Tobias Brixner, this is the credo of optical spectroscopy....

Anzeige

Anzeige

Event News

Leading experts in Diabetes, Metabolism and Biomedical Engineering discuss Precision Medicine

13.07.2018 | Event News

Conference on Laser Polishing – LaP: Fine Tuning for Surfaces

12.07.2018 | Event News

11th European Wood-based Panel Symposium 2018: Meeting point for the wood-based materials industry

03.07.2018 | Event News

Latest News

A smart safe rechargeable zinc ion battery based on sol-gel transition electrolytes

20.07.2018 | Power and Electrical Engineering

Reversing cause and effect is no trouble for quantum computers

20.07.2018 | Information Technology

Princeton-UPenn research team finds physics treasure hidden in a wallpaper pattern

20.07.2018 | Materials Sciences

VideoLinks

Science & Research

Science & Research

NASA | A Year in the Life of Earth's CO2

NASA Computer Model Provides a New Portrait of Carbon Dioxide

Black Holes Come to the Big Screen

The new movie "Interstellar" explores a longstanding fascination, but UA astrophysicists are using cutting-edge technology to go one better.

NASA's Swift Mission Observes Mega Flares from a Mini Star

NASA's Swift satellite detected the strongest, hottest, and longest-lasting sequence of stellar flares ever seen from a nearby red dwarf star.

NASA | Global Hawks Soar into Storms

NASA's airborne Hurricane and Severe Storm Sentinel or HS3 mission, will revisit the Atlantic Ocean for the third year in a row.

Baffin Island - Disappearing ice caps

Giff Miller, geologist and paleoclima-tologist, is walking the margins of melting glaciers on Baffin Island, Nunavut, Canada.

The Infrasound Network and how it works

The CTBTO uses infrasound stations to monitor the Earth mainly for atmospheric explosions.