Misplaced Pages

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 artificial intelligence research to create smaller, explicit, new proofs of mathematical theorems from the bottom up using automated 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 human-readable proofs which are nonetheless formally verified for correctness. Since these proofs are generally human-surveyable (albeit with difficulty, as with the proof of the 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 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 ${\displaystyle (+,-,\times ,/)}$. 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.

Philosophical objections

This section needs additional citations for verification. Please help improve this article by adding citations to reliable sources in this section. Unsourced material may be challenged and removed. (October 2020) (Learn how and when to remove this message)

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

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.

• Common fixed point problem, 1967
• Four color theorem, 1976
• Mitchell Feigenbaum's universality conjecture in non-linear dynamics. Proven by O. E. Lanford using rigorous computer arithmetic, 1982
• Connect Four, 1988 – a solved game
• Non-existence of a finite projective plane of order 10, 1989
• Double bubble conjecture, 1995
• Robbins conjecture, 1996
• Kepler conjecture, 1998 – the problem of optimal sphere packing in a box
• Lorenz attractor, 2002 – 14th of Smale's problems proved by Warwick Tucker using interval arithmetic
• 17-point case of the Happy Ending problem, 2006
• Kouril (between 2006 and 2016) computed several van der Waerden numbers using FPGA-based SAT-solver.
• NP-hardness of minimum-weight triangulation, 2008
• Ahmed (between 2009 and 2014) computed several van der Waerden numbers using DPLL algorithm-based stand-alone and distributed SAT-solvers. Ahmed first used cluster-distributed SAT-solvers to prove w(2; 3, 17) = 279 and w(2; 3, 18) = 312 in 2010.
• Optimal solutions for Rubik's Cube can be obtained in at most 20 face moves, 2010
• Minimum number of clues for a solvable Sudoku puzzle is 17, 2012
• In 2014 a special case of the Erdős discrepancy problem was solved using a SAT-solver. The full conjecture was later solved by Terence Tao without computer assistance.
• Boolean Pythagorean triples problem solved using 200 terabytes of data in May 2016.
• Applications to the Kolmogorov-Arnold-Moser theory
• Kazhdan's property (T) for the automorphism group of a free group of rank at least five
• Schur number five, the proof that S(5) = 161 was announced in 2017 by Marijn Heule and took up 2 petabytes of space
• Keller's conjecture in dimension 7 the only remaining case in 2020 with a 200 gigabyte proof
• The packing chromatic number of the infinite square grid is 15, by Subercaseaux and Heule in 2023 (See also: Hadwiger–Nelson problem for the chromatic number of the plane)

See also

• Formal verification – Proving or disproving the correctness of certain intended algorithms
• Logic Theorist – 1956 computer program written by Allen Newell, Herbert A. Simon and Cliff Shaw
• Mathematical proof – Reasoning for mathematical statements
• Metamath – Formal language and associated computer program
• Model checking – Computer science field
• Seventeen or Bust – BOINC based volunteer computing project researching prime numbersPages displaying short descriptions of redirect targets
• Symbolic computation – Scientific area at the interface between computer science and mathematicsPages displaying short descriptions of redirect targets
• Validated numerics – numerics including mathematically strict error evaluationPages displaying wikidata descriptions as a fallback

References

1. Tymoczko, Thomas (1979), "The Four-Color Problem and its Mathematical Significance", The Journal of Philosophy, 76 (2): 57–83, doi:10.2307/2025976, JSTOR 2025976.
2. Boyce, William M. (March 1969). "Commuting Functions with No Common Fixed Point" (PDF). Transactions of the American Mathematical Society. 137: 77–92. doi:10.1090/S0002-9947-1969-0236331-5.
3. Gonthier, Georges (2008), "Formal Proof—The Four-Color Theorem" (PDF), Notices of the American Mathematical Society, 55 (11): 1382–1393, MR 2463991, archived (PDF) from the original on 2011-08-05
4. Hass, J.; Hutchings, M.; Schlafly, R. (1995). "The double bubble conjecture". Electronic Research Announcements of the American Mathematical Society. 1 (3): 98–102. CiteSeerX 10.1.1.527.8616. doi:10.1090/S1079-6762-95-03001-0.
5. 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.
6. Kouril, Michal (2012). "Computing the van der Waerden number W(3,4)=293". Integers. 12: A46. MR 3083419.
7. Kouril, Michal (2015). "Leveraging FPGA clusters for SAT computations". Parallel Computing: On the Road to Exascale: 525–532.
8. Ahmed, Tanbir (2009). "Some new van der Waerden numbers and some van der Waerden-type numbers". Integers. 9: A6. doi:10.1515/integ.2009.007. MR 2506138. S2CID 122129059.
9. ^ Ahmed, Tanbir (2010). "Two new van der Waerden numbers w(2;3,17) and w(2;3,18)". Integers. 10 (4): 369–377. doi:10.1515/integ.2010.032. MR 2684128. S2CID 124272560.
10. Ahmed, Tanbir (2012). "On computation of exact van der Waerden numbers". Integers. 12 (3): 417–425. doi:10.1515/integ.2011.112. MR 2955523. S2CID 11811448.
11. Ahmed, Tanbir (2013). "Some More Van der Waerden numbers". Journal of Integer Sequences. 16 (4): 13.4.4. MR 3056628.
12. Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter (2014). "On the van der Waerden numbers w(2;3,t)". Discrete Applied Mathematics. 174 (2014): 27–51. arXiv:1102.5433. doi:10.1016/j.dam.2014.05.007. MR 3215454.
13. "God's Number is 20". cube20.org. July 2010. Retrieved 2023-10-18.
14. Cesare, Chris (1 October 2015). "Maths whizz solves a master's riddle". Nature. 526 (7571): 19–20. Bibcode:2015Natur.526...19C. doi:10.1038/nature.2015.18441. PMID 26432222.
15. Lamb, Evelyn (26 May 2016). "Two-hundred-terabyte maths proof is largest ever". Nature. 534 (7605): 17–18. Bibcode:2016Natur.534...17L. doi:10.1038/nature.2016.19990. PMID 27251254.
16. Celletti, A.; Chierchia, L. (1987). "Rigorous estimates for a computer-assisted KAM theory". Journal of Mathematical Physics. 28 (9): 2078–86. Bibcode:1987JMP....28.2078C. doi:10.1063/1.527418.
17. Figueras, J.L.; Haro, A.; Luque, A. (2017). "Rigorous computer-assisted application of KAM theory: a modern approach". Foundations of Computational Mathematics. 17 (5): 1123–93. arXiv:1601.00084. doi:10.1007/s10208-016-9339-3. hdl:2445/192693. S2CID 28258285.
18. Heule, Marijn J. H. (2017). "Schur Number Five". arXiv:1711.08076 .
19. "Schur Number Five". www.cs.utexas.edu. Retrieved 2021-10-06.
20. Brakensiek, Joshua; Heule, Marijn; Mackey, John; Narváez, David (2020). "The Resolution of Keller's Conjecture". In Peltier, Nicolas; Sofronie-Stokkermans, Viorica (eds.). Automated Reasoning. Lecture Notes in Computer Science. Vol. 12166. Springer. pp. 48–65. doi:10.1007/978-3-030-51074-9_4. ISBN 978-3-030-51074-9. PMC 7324133.
21. Hartnett, Kevin (2020-08-19). "Computer Search Settles 90-Year-Old Math Problem". Quanta Magazine. Retrieved 2021-10-08.
22. Subercaseaux, Bernardo; Heule, Marijn J. H. (2023-01-23). "The Packing Chromatic Number of the Infinite Square Grid is 15". arXiv:2301.09757 .
23. Hartnett, Kevin (2023-04-20). "The Number 15 Describes the Secret Limit of an Infinite Grid". Quanta Magazine. Retrieved 2023-04-20.

Further reading

• Lenat, D.B. (1976). AM: An artificial intelligence approach to discovery in mathematics as heuristic search (PDF) (PhD). AI Lab., Stanford University. STAN-CS-76-570, Heuristic Programming Project Report HPP-76-8.
• Meyer, K.R.; Schmidt, D.S., eds. (2012). Computer aided proofs in analysis. IMA volumes in mathematics and its applications. Vol. 28. Springer. ISBN 978-1-4613-9092-3.
• Nakao, M.; Plum, M.; Watanabe, Y. (2019). Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations. Springer Series in Computational Mathematics. Springer. ISBN 9789811376696.

External links

• Lanford, Oscar E. (1982). "A computer-assisted proof of the Feigenbaum conjectures" (PDF). Bull. Amer. Math. Soc. 6 (3): 427–434. CiteSeerX 10.1.1.434.8389. doi:10.1090/S0273-0979-1982-15008-X.
• Furse, Edmund (1990). Why did AM run out of steam? (Technical report). Department of Computer Studies, University of Glamorgan. CS-90-4. Archived from the original on 2012-07-17. Retrieved 2016-09-06.{{cite tech report}}: CS1 maint: bot: original URL status unknown (link)
• Begley, S. (April 16, 2018). "Number proofs done by computer might err". Pittsburgh Post-Gazette. Archived from the original on 2018-04-16.
• "A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008.

v t e Mathematical logic
General	Axiom list Cardinality First-order logic Formal proof Formal semantics Foundations of mathematics Information theory Lemma Logical consequence Model Theorem Theory Type theory
Theorems (list)  and paradoxes	Gödel's completeness and incompleteness theorems Tarski's undefinability Banach–Tarski paradox Cantor's theorem, paradox and diagonal argument Compactness Halting problem Lindström's Löwenheim–Skolem Russell's paradox
Logics	Traditional Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram Propositional Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞ Predicate First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus
Set theory	Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities Types of sets Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann Maps and cardinality Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary Set theories Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive
Formal systems (list), language and syntax	Alphabet Arity Automata Axiom schema Expression ground Extension by definition conservative Relation Formation rule Grammar Formula atomic closed ground open Free/bound variable Language Metalanguage Logical connective ¬ ∨ ∧ → ↔ = Predicate functional variable propositional variable Proof Quantifier ∃ ! ∀ rank Sentence atomic spectrum Signature String Substitution Symbol function logical/constant non-logical variable Term Theory list Example axiomatic systems (list) of arithmetic: Peano second-order elementary function primitive recursive Robinson Skolem of the real numbers Tarski's axiomatization of Boolean algebras canonical minimal axioms of geometry: Euclidean: Elements Hilbert's Tarski's non-Euclidean Principia Mathematica
Proof theory	Formal proof Natural deduction Logical consequence Rule of inference Sequent calculus Theorem Systems axiomatic deductive Hilbert list Complete theory Independence (from ZFC) Proof of impossibility Ordinal analysis Reverse mathematics Self-verifying theories
Model theory	Interpretation function of models Model equivalence finite saturated spectrum submodel Non-standard model of arithmetic Diagram elementary Categorical theory Model complete theory Satisfiability Semantics of logic Strength Theories of truth semantic Tarski's Kripke's T-schema Transfer principle Truth predicate Truth value Type Ultraproduct Validity
Computability theory	Church encoding Church–Turing thesis Computably enumerable Computable function Computable set Decision problem decidable undecidable P NP P versus NP problem Kolmogorov complexity Lambda calculus Primitive recursive function Recursion Recursive set Turing machine Type theory
Related	Abstract logic Algebraic logic Automated theorem proving Category theory Concrete/Abstract category Category of sets History of logic History of mathematical logic timeline Logicism Mathematical object Philosophy of mathematics Supertask
Mathematics portal

• Argument technology
• Automated theorem proving
• Computer-assisted proofs
• Formal methods
• Numerical analysis
• Philosophy of mathematics