Computer-assisted proof

A computer-assisted proof is a mathematical proof that has been generated by computer.

Most computer-aided proofs to date have been implementions of proof-by-exhaustion of a mathematical theorem. The four color theorem was the first major theorem to be proved using a computer.

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. The most famous of these efforts was Douglas Lenat's 1976 program AM ("a mathematician"). However, beyond discovering some new proofs of some elementary mathematical theorems, this approach has not had any significant success.

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 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 computer programming.

The reverse question can also be raised: if computers cannot be trusted to carry out lengthy calculations, since human beings are by no means infallible, why do some mathematicans place greater trust in lengthy human reasoning compared to similarly lengthy machine computation?

Other mathematicians believe that lengthy computer-assisted proofs are no more or less valid than any other type of proof, and that the problem of human verifiability can be addressed by proving the proof program itself valid. 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 using an automated theorem prover to demonstrate their correctness. Understandably, the approach of using computer programs to prove other computer programs correct does not appeal to computer proof skeptics, who simply see it as adding another layer of complication without addressing the fundamental issue of the need for human understanding.

Another argument against computer-aided proofs is that they lack mathematical elegance: however, this is an argument that is not restricted to computer proofs, but can also be advanced against any lengthy proof by exhaustion. A similar argument against computer-aided proofs and proofs-by-exhaustion is they provide no insights or new and useful concepts.

A more interesting philosophical issue raised by computer-aided proofs is whether they make mathematics into an experimental science, where the scientific method becomes more important than the application of pure reason on a Platonic realm of 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, 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.

Massively parallel proof-by-exhaustion projects

Seventeen or Bust is a computer-aided attack on the Sierpinski problem currently taking place using distributed computation on the Internet.

See also

• Automated theorem proving
• Symbolic mathematics
• Experimental mathematics
• 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, 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