 Computerassisted proof

A computerassisted proof is a mathematical proof that has been at least partially generated by computer.
Most computeraided proofs to date have been implementations of large proofsbyexhaustion 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 humanreadable proofs which are nonetheless formally verified for correctness. Since these proofs are generally humansurveyable (albeit with difficulty, as with the proof of the Robbins conjecture) they do not share the controversial implications of computeraided proofsbyexhaustion.
Contents
Methods
One method used in proofs involving numeric calculations is to control the roundoff 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
Computerassisted proofs are the subject of much controversy in the mathematical world. Some mathematicians believe that lengthy computerassisted proofs are not, in some sense, 'real' mathematical proofs 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 computerassisted 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é^{[citation needed]}. Arguments that computerassisted 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 fourcolor theorem in 2005) as well as replicating the result using different programming languages, different compilers, and different computer hardware.
Another possible way of verifying computeraided proofs is to generate their reasoning steps in a machinereadable 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 computeraided 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 computeraided proofs is whether they make mathematics into a quasiempirical 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 computeraided 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 twentyfirst century theoretical physics is becoming too mathematical, and leaving behind its experimental roots.
The emerging field of experimental mathematics is confronting this debate headon by focusing on numerical experiments as its main tool for mathematical exploration.
Theorems for sale
In 2010, academics at The University of Edinburgh offered people the chance to "buy their own theorem" created through a computerassisted proof. This new theorem would be named after the purchaser.^{[1]}
List of theorems proved with the help of computer programs
Inclusion in this list does not imply that a formal computerchecked proof exists, but rather, that a computer program has been involved in some way. See the main articles for details.
 Four color theorem, 1976
 Connect Four, 1988 – a game
 Nonexistence of a finite projective plane of order 10, 1989
 Robbins conjecture, 1996
 Kepler conjecture, 1998 – the problem of optimal sphere packing in a box. Not yet definitively proved.
 17point case of the Happy Ending problem, 2006
See also
 Symbolic mathematics
 Model checking
 Proof checking
 Automated reasoning
 Formal verification
 Observational science
 Garbage in, garbage out
Further reading
 Lenat, D.B., (1976), AM: An artificial intelligence approach to discovery in mathematics as heuristic search, Ph.D. Thesis, STANCS76570, and Heuristic Programming Project Report HPP768, Stanford University, AI Lab., Stanford, CA.
References
 ^ "Herald Gazette article on buying your own theorem". Herald Gazette Scotland. November 2010. http://www.heraldscotland.com/news/education/yourownmathstheoremfor151.1068654.
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
"A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008. http://www.ams.org/notices/200811/.
Wikimedia Foundation. 2010.
Look at other dictionaries:
Computeraided — or computer assisted is a prefix that hints to the use of a computer as an indispensable tool in a certain field, usually derived from more traditional fields of science and engineering. Instead of the prefix computer aided or computer assisted,… … Wikipedia
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 proved separately. A… … Wikipedia
Computer security — This article is about computer security through design and engineering. For computer security exploits and defenses, see computer insecurity. Computer security Secure operating systems Security architecture Security by design Secure coding … Wikipedia
Mathematical proof — In mathematics, a proof is a convincing demonstration (within the accepted standards of the field) that some mathematical statement is necessarily true.[1][2] Proofs are obtained from deductive reasoning, rather than from inductive or empirical… … Wikipedia
Optimal solutions for Rubik's Cube — Computer Graphics of a scrambled Rubik s cube There are many algorithms to solve scrambled Rubik s Cubes. The maximum number of face turns needed to solve any instance of the Rubik s cube is 20.[1] This number is also known as the diameter of the … Wikipedia
Four color theorem — Example of a four colored map A four colori … Wikipedia
Metamath — Developer(s) Norman Megill Written in C Operating system … Wikipedia
Equichordal point problem — In Euclidean plane geometry, the equichordal point problem is the question whether a closed planar convex body can have two equichordal points.[1] The problem was originally posed in 1916 by Fujiwara and in 1917 by Wilhelm Blaschke, Rothe and… … Wikipedia
Experimental mathematics — For the mathematical journal of the same name, see Experimental Mathematics (journal) Experimental mathematics is an approach to mathematics in which numerical computation is used to investigate mathematical objects and identify properties and… … Wikipedia
Oren Patashnik — (born 1954) is a computer scientist. He is notable for co creating BibTeX, and co writing Concrete Mathematics: A Foundation for Computer Science.[1] He is a researcher at the Center for Communications Research, La Jolla. History Oren Patashnik… … Wikipedia