Computer-assisted proof

Source: Wikipedia, the free 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

Robbins conjecture
) they do not share the controversial implications of computer-aided proofs-by-exhaustion.

Methods

One method for using computers in mathematical proofs is by means of so-called validated numerics or rigorous numerics. This means computing numerically yet with mathematical rigour. One uses set-valued arithmetic and inclusion principle[clarify] in order to ensure that the set-valued output of a numerical program encloses the solution of the original mathematical problem. This is done by controlling, enclosing and propagating round-off and truncation errors using for example interval arithmetic. More precisely, one reduces the computation to a sequence of elementary operations, say . In a computer, the result of each 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.[citation needed]

Philosophical objections

Main article: Non-surveyable proof

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.[1]

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

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.

Applications

Theorems proved with the help of computer programs

See also: Proof assistant § Notable formalized proofs

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.

See also

References

  1. JSTOR 2025976
    .
  2. MR 2463991, archived
    (PDF) from the original on 2011-08-05
  3. doi:10.1090/S1079-6762-95-03001-0
    .
  4. ^ Kouril, Michal (2006). A Backtracking Framework for Beowulf Clusters with an Extension to Multi-Cluster Computation and Sat Benchmark Problem Implementation (Ph.D. thesis). University of Cincinnati.
  5. ^ Kouril, Michal (2012). "Computing the van der Waerden number W(3,4)=293". Integers. 12: A46.
    MR 3083419
    .
  6. ^ Kouril, Michal (2015). "Leveraging FPGA clusters for SAT computations". Parallel Computing: On the Road to Exascale: 525–532.
  7. ^ Ahmed, Tanbir (2009). "Some new van der Waerden numbers and some van der Waerden-type numbers". Integers. 9: A6.
    S2CID 122129059
    .
  8. ^ a b Ahmed, Tanbir (2010). "Two new van der Waerden numbers w(2;3,17) and w(2;3,18)". Integers. 10 (4): 369–377.
    S2CID 124272560
    .
  9. ^ Ahmed, Tanbir (2012). "On computation of exact van der Waerden numbers". Integers. 12 (3): 417–425.
    S2CID 11811448
    .
  10. ^ Ahmed, Tanbir (2013). "Some More Van der Waerden numbers". Journal of Integer Sequences. 16 (4): 13.4.4.
    MR 3056628
    .
  11. ^ Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter (2014). "On the van der Waerden numbers w(2;3,t)".
    MR 3215454
    .
  12. ^ "God's Number is 20". cube20.org. July 2010. Retrieved 2023-10-18.
  13. PMID 26432222
    .
  14. PMID 27251254
    .
  15. doi:10.1063/1.527418
    .
  16. S2CID 28258285
    .
  17. arXiv:1711.08076 [cs.LO
    ].
  18. ^ "Schur Number Five". www.cs.utexas.edu. Retrieved 2021-10-06.
  19. PMC 7324133
    .
  20. ^ Hartnett, Kevin (2020-08-19). "Computer Search Settles 90-Year-Old Math Problem". Quanta Magazine. Retrieved 2021-10-08.
  21. arXiv:2301.09757 [cs.DM
    ].
  22. ^ Hartnett, Kevin (2023-04-20). "The Number 15 Describes the Secret Limit of an Infinite Grid". Quanta Magazine. Retrieved 2023-04-20.

Further reading

External links
Retrieved from "https://en.wikipedia.org/w/index.php?title=Computer-assisted_proof&oldid=1199019976"