Computer-assisted proof

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 four color theorem was the first major theorem to be proved using a computer. The idea of computer-assisted proofs is to use the computer to perform lengthy computations, but to verify the correctness of the program separately.

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, some interactive proof assistants allow mathematicians to develop human-readable proofs which are nonetheless formally verified for correctness. These areas do not share the controversial implications of computer-aided proofs-by-exhaustion.

1 Methods 2 Philosophical objections 3 See also 4 Further reading 5 External links

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.

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 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 put their trust in an empirical computational process instead of logical deduction from assumed axioms.

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é. They reply to their opponents' arguments that computer-assisted proofs are subject to errors in their source programs, compilers, and hardware, can be resolved by multiple replications of 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.

As of 2005^[update], there is an emerging field of experimental mathematics that is confronting this debate head-on by focusing on numerical experiments as its main tool for mathematical exploration.

• Automated theorem proving
• Symbolic mathematics
• Model checking
• Proof checking
• Automated reasoning
• Formal verification
• Experimental mathematics
• Observational science
• Garbage in, garbage out

• 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.

• 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).