Computer-assisted proofs are the subject of some controversy in the mathematical world, with
Thomas Tymoczko first to articulate objections. Those who adhere to Tymoczko's arguments 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 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". 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 a
proof checker program to demonstrate their correctness. Since validating a given proof is much easier than finding a proof, the checker program is simpler than the original assistant program, and it is correspondingly easier to gain confidence into its correctness. However, this approach of using a computer program to prove the output of 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. 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. == Theorems proved with the help of computer programs ==