Computer-assisted proof
Encyclopedia
A computer-assisted proof is a mathematical proof
that has been at least partially generated by computer.
Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion
of a mathematical theorem
. The idea is to use a computer program to perform lengthy computations, and to provide a proof that the result of these computations implies the given theorem. In 1976, the four color theorem
was the first major theorem to be verified using a computer program.
Attempts have also been made in the area of artificial intelligence
research to create smaller, explicit, new proofs of mathematical theorems from the bottom up using machine reasoning techniques such as heuristic search. Such automated theorem provers have proved a number of new results and found new proofs for known theorems. Additionally, interactive proof assistants allow mathematicians to develop human-readable proofs which are nonetheless formally verified for correctness. Since these proofs are generally human-surveyable (albeit with difficulty, as with the proof of the Robbins conjecture) they do not share the controversial implications of computer-aided proofs-by-exhaustion.
s because they involve so many logical steps that they are not practically verifiable by human beings, and that mathematicians are effectively being asked to replace logical deduction from assumed axioms with trust in an empirical computational process, which is potentially affected by errors in the computer program, as well as defects in the runtime environment and hardware.
Other mathematicians believe that lengthy computer-assisted proofs should be regarded as calculations, rather than proofs: the proof algorithm itself should be proved valid, so that its use can then be regarded as a mere "verification". This is known as "Poincaré's principle" in the mathematical community, after a statement by Henri Poincaré
. Arguments that computer-assisted proofs are subject to errors in their source programs, compilers, and hardware can be resolved by providing a formal proof of correctness for the computer program (an approach which was successfully applied to the four-color theorem in 2005) as well as replicating the result using different programming languages, different compilers, and different computer hardware.
Another possible way of verifying computer-aided proofs is to generate their reasoning steps in a machine-readable form, and then use an automated theorem prover to demonstrate their correctness. This approach of using a computer program to prove another program correct does not appeal to computer proof skeptics, who see it as adding another layer of complexity without addressing the perceived need for human understanding.
Another argument against computer-aided proofs is that they lack mathematical elegance—that they provide no insights or new and useful concepts. In fact, this is an argument that could be advanced against any lengthy proof by exhaustion.
An additional philosophical issue raised by computer-aided proofs is whether they make mathematics into a quasi-empirical science
, where the scientific method
becomes more important than the application of pure reason in the area of abstract mathematical concepts. This directly relates to the argument within mathematics as to whether mathematics is based on ideas, or "merely" an exercise in formal symbol manipulation. It also raises the question whether, if according to the Platonist view, all possible mathematical objects in some sense "already exist", whether computer-aided mathematics is an observational science
like astronomy, rather than an experimental one like physics or chemistry. Interestingly, this controversy within mathematics is occurring at the same time as questions are being asked in the physics community about whether twenty-first century theoretical physics
is becoming too mathematical, and leaving behind its experimental roots.
The emerging field of experimental mathematics
is confronting this debate head-on by focusing on numerical experiments as its main tool for mathematical exploration.
offered people the chance to "buy their own theorem" created through a computer-assisted proof. This new theorem would be named after the purchaser.
Mathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
that has been at least partially generated by computer.
Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion
Proof by exhaustion
Proof by exhaustion, also known as proof by cases, perfect induction, or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases and each case is checked to see if the proposition in question holds...
of a mathematical theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
. The idea is to use a computer program to perform lengthy computations, and to provide a proof that the result of these computations implies the given theorem. In 1976, the four color theorem
Four color theorem
In mathematics, the four color theorem, or the four color map theorem states that, given any separation of a plane into contiguous regions, producing a figure called a map, no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color...
was the first major theorem to be verified using a computer program.
Attempts have also been made in the area of artificial intelligence
Artificial intelligence
Artificial intelligence is the intelligence of machines and the branch of computer science that aims to create it. AI textbooks define the field as "the study and design of intelligent agents" where an intelligent agent is a system that perceives its environment and takes actions that maximize its...
research to create smaller, explicit, new proofs of mathematical theorems from the bottom up using machine reasoning techniques such as heuristic search. Such automated theorem provers have proved a number of new results and found new proofs for known theorems. Additionally, interactive proof assistants allow mathematicians to develop human-readable proofs which are nonetheless formally verified for correctness. Since these proofs are generally human-surveyable (albeit with difficulty, as with the proof of the Robbins conjecture) they do not share the controversial implications of computer-aided proofs-by-exhaustion.
Methods
One method used in proofs involving numeric calculations is to control the round-off and propagation errors through the interval arithmetic technique. More precisely, one reduces the computation to a sequence of elementary operations, say (+,-,*,/); the result of an elementary operation is rounded off by the computer precision. However, one can construct an interval provided by upper and lower bounds on the result of an elementary operation. Then one proceeds by replacing numbers with intervals and performing elementary operations between such intervals of representable numbers.Philosophical objections
Computer-assisted proofs are the subject of much controversy in the mathematical world. Some mathematicians believe that lengthy computer-assisted proofs are not, in some sense, 'real' mathematical proofMathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
s because they involve so many logical steps that they are not practically verifiable by human beings, and that mathematicians are effectively being asked to replace logical deduction from assumed axioms with trust in an empirical computational process, which is potentially affected by errors in the computer program, as well as defects in the runtime environment and hardware.
Other mathematicians believe that lengthy computer-assisted proofs should be regarded as calculations, rather than proofs: the proof algorithm itself should be proved valid, so that its use can then be regarded as a mere "verification". This is known as "Poincaré's principle" in the mathematical community, after a statement by Henri Poincaré
Henri Poincaré
Jules Henri Poincaré was a French mathematician, theoretical physicist, engineer, and a philosopher of science...
. Arguments that computer-assisted proofs are subject to errors in their source programs, compilers, and hardware can be resolved by providing a formal proof of correctness for the computer program (an approach which was successfully applied to the four-color theorem in 2005) as well as replicating the result using different programming languages, different compilers, and different computer hardware.
Another possible way of verifying computer-aided proofs is to generate their reasoning steps in a machine-readable form, and then use an automated theorem prover to demonstrate their correctness. This approach of using a computer program to prove another program correct does not appeal to computer proof skeptics, who see it as adding another layer of complexity without addressing the perceived need for human understanding.
Another argument against computer-aided proofs is that they lack mathematical elegance—that they provide no insights or new and useful concepts. In fact, this is an argument that could be advanced against any lengthy proof by exhaustion.
An additional philosophical issue raised by computer-aided proofs is whether they make mathematics into a quasi-empirical science
Quasi-empiricism in mathematics
Quasi-empiricism in mathematics is the attempt in the philosophy of mathematics to direct philosophers' attention to mathematical practice, in particular, relations with physics, social sciences, and computational mathematics, rather than solely to issues in the foundations of mathematics...
, where the scientific method
Scientific method
Scientific method refers to a body of techniques for investigating phenomena, acquiring new knowledge, or correcting and integrating previous knowledge. To be termed scientific, a method of inquiry must be based on gathering empirical and measurable evidence subject to specific principles of...
becomes more important than the application of pure reason in the area of abstract mathematical concepts. This directly relates to the argument within mathematics as to whether mathematics is based on ideas, or "merely" an exercise in formal symbol manipulation. It also raises the question whether, if according to the Platonist view, all possible mathematical objects in some sense "already exist", whether computer-aided mathematics is an observational science
Observational science
An observational science is a science where it is not possible to construct controlled experiments in the area under study. For example, in astronomy, it is not possible to create or manipulate stars or galaxies in order to observe what happens...
like astronomy, rather than an experimental one like physics or chemistry. Interestingly, this controversy within mathematics is occurring at the same time as questions are being asked in the physics community about whether twenty-first century theoretical physics
Theoretical physics
Theoretical physics is a branch of physics which employs mathematical models and abstractions of physics to rationalize, explain and predict natural phenomena...
is becoming too mathematical, and leaving behind its experimental roots.
The emerging field of experimental mathematics
Experimental mathematics
Experimental mathematics is an approach to mathematics in which numerical computation is used to investigate mathematical objects and identify properties and patterns...
is confronting this debate head-on by focusing on numerical experiments as its main tool for mathematical exploration.
Theorems for sale
In 2010, academics at The University of EdinburghUniversity of Edinburgh
The University of Edinburgh, founded in 1583, is a public research university located in Edinburgh, the capital of Scotland, and a UNESCO World Heritage Site. The university is deeply embedded in the fabric of the city, with many of the buildings in the historic Old Town belonging to the university...
offered people the chance to "buy their own theorem" created through a computer-assisted proof. This new theorem would be named after the purchaser.
List of theorems proved with the help of computer programs
Inclusion in this list does not imply that a formal computer-checked proof exists, but rather, that a computer program has been involved in some way. See the main articles for details.- Four color theoremFour color theoremIn mathematics, the four color theorem, or the four color map theorem states that, given any separation of a plane into contiguous regions, producing a figure called a map, no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color...
, 1976 - Connect FourConnect FourConnect Four is a two-player game in which the players first choose a color and then take turns dropping their colored discs from the top into a seven-column, six-row vertically-suspended grid...
, 1988 – a game - Non-existence of a finite projective planeProjective planeIn mathematics, a projective plane is a geometric structure that extends the concept of a plane. In the ordinary Euclidean plane, two lines typically intersect in a single point, but there are some pairs of lines that do not intersect...
of order 10, 1989 - Robbins conjecture, 1996
- Kepler conjectureKepler conjectureThe Kepler conjecture, named after the 17th-century German astronomer Johannes Kepler, is a mathematical conjecture about sphere packing in three-dimensional Euclidean space. It says that no arrangement of equally sized spheres filling space has a greater average density than that of the cubic...
, 1998 – the problem of optimal sphere packing in a box. Not yet definitively proved. - 17-point case of the Happy Ending problemHappy Ending problemThe Happy Ending problem is the following statement:This was one of the original results that led to the development of Ramsey theory....
, 2006
See also
- Symbolic mathematics
- Model checkingModel checkingIn computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
- Proof checkingProof checkingAutomated proof checking is the process of using software for checking proofs for correctness. It is one of the most developed fields in automated reasoning....
- Automated reasoningAutomated reasoningAutomated reasoning is an area of computer science dedicated to understand different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically...
- Formal verificationFormal verificationIn the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
- Observational scienceObservational scienceAn observational science is a science where it is not possible to construct controlled experiments in the area under study. For example, in astronomy, it is not possible to create or manipulate stars or galaxies in order to observe what happens...
- Garbage in, garbage outGarbage In, Garbage OutGarbage in, garbage out is a phrase in the field of computer science or information and communication technology. It is used primarily to call attention to the fact that computers will unquestioningly process the most nonsensical of input data and produce nonsensical output...
Further reading
- Lenat, D.B., (1976), AM: An artificial intelligence approach to discovery in mathematics as heuristic search, Ph.D. Thesis, STAN-CS-76-570, and Heuristic Programming Project Report HPP-76-8, Stanford University, AI Lab., Stanford, CA.
External links
- Edmund Furse; Why did AM run out of steam?
- Keith Devlin; Last doubts removed about the proof of the Four Color Theorem, MAA Online, January 2005
- Number proofs done by computer might err