Editing Computer-assisted proof

{{Short description|Mathematical proof at least partially generated by computer}}

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 [[Proof by exhaustion|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 (computer science)|heuristic]] search. Such [[automated theorem prover]]s have proved a number of new results and found new proofs for known theorems.{{Citation needed|date=August 2016}}  Additionally, interactive [[proof assistant]]s allow mathematicians to develop human-readable proofs which are nonetheless formally verified for correctness.  Since these proofs are generally [[Non-surveyable proof|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 {{clarify span|inclusion principle|reason=What is this supposed to mean?|date=October 2020}} 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 <math>(+, -, \times, /)</math>. 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|reason=Give some typical usages of this method. How can nontrivial theorems, involving variables and quantifiers, be proven just by computation?|date=October 2020}}

==Philosophical objections==
{{main|Non-surveyable proof}}
{{More citations needed section|date=October 2020}}

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 proof]]s because they involve so many logical steps that they are not practically [[Verification and validation|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.<ref name="tymoczko">{{Citation|last = Tymoczko|first = Thomas|author-link = Thomas Tymoczko|title = The Four-Color Problem and its Mathematical Significance|year = 1979|journal = [[The Journal of Philosophy]]|volume = 76|issue = 2|pages = 57–83|doi=10.2307/2025976|jstor = 2025976}}.</ref>

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-empiricism in mathematics|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 (mathematics)|exercise]] in formal symbol manipulation. It also raises the question whether, if according to the [[mathematical Platonism|Platonist]] view, all possible mathematical objects in some sense "already exist", whether computer-aided mathematics is an [[observational study|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 ==
{{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.

{{columns-list|colwidth=22em|1=* [[Common fixed point problem]], 1967<ref>{{Cite journal |last=Boyce |first=William M. |date=March 1969 |title=Commuting Functions with No Common Fixed Point |url=https://www.ams.org/journals/tran/1969-137-00/S0002-9947-1969-0236331-5/S0002-9947-1969-0236331-5.pdf |journal=Transactions of the American Mathematical Society |volume=137 |pages=77-92 |doi=10.1090/S0002-9947-1969-0236331-5}}</ref>
* [[Four color theorem]], 1976<ref>{{Citation |last=Gonthier |first=Georges |author-link=Georges Gonthier |title=Formal Proof—The Four-Color Theorem |journal=[[Notices of the American Mathematical Society]] |volume=55 |year=2008 |url=https://www.ams.org/notices/200811/tx081101382p.pdf |archive-url=https://web.archive.org/web/20110805094909/http://www.ams.org/notices/200811/tx081101382p.pdf |archive-date=2011-08-05 |url-status=live |issue=11 |pages=1382–1393 |mr=2463991 }}</ref>
* [[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<ref>{{cite journal |last1=Hass |first1=J. |last2=Hutchings |first2=M. |last3=Schlafly |first3=R. |title=The double bubble conjecture |journal=Electronic Research Announcements of the American Mathematical Society |volume=1 |issue=3 |pages=98–102 |date=1995 |doi=10.1090/S1079-6762-95-03001-0 |url=https://www.ams.org/era/1995-01-03/S1079-6762-95-03001-0/ |citeseerx=10.1.1.527.8616 }}</ref>
* [[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<ref name=kouril2006>
{{
cite thesis
| last = Kouril
| first=Michal
| title= A Backtracking Framework for Beowulf Clusters with an Extension to Multi-Cluster Computation and Sat Benchmark Problem Implementation
| degree=Ph.D.
| publisher=University of Cincinnati
| year = 2006
| url = http://rave.ohiolink.edu/etdc/view?acc_num=ucin1163607141
}}
</ref><ref name=kouril2012>
{{
cite journal
| last = Kouril
| first=Michal
| title= Computing the van der Waerden number W(3,4)=293
| journal = Integers
| volume = 12
| year = 2012
| pages = A46
| mr = 3083419
}}
</ref><ref name=kouril2016>
{{
cite journal
| last = Kouril
| first=Michal
| title= Leveraging FPGA clusters for SAT computations
| journal = Parallel Computing: On the Road to Exascale
| year = 2015
| pages = 525–532
}}
</ref> (between 2006 and 2016) computed several [[van der Waerden number]]s using [[FPGA]]-based [[SAT-solver]].
* [[NP-hard]]ness of [[minimum-weight triangulation]], 2008
* Ahmed<ref name=ahmed2009>
{{
cite journal
| last = Ahmed
| first=Tanbir
| title=Some new van der Waerden numbers and some van der Waerden-type numbers
| journal = Integers
| volume = 9
| year = 2009
| pages = A6
| doi=10.1515/integ.2009.007
| mr = 2506138
| s2cid=122129059
}}
</ref><ref name=ahmed2010>
{{
cite journal
| last = Ahmed
| first=Tanbir
| title= Two new van der Waerden numbers w(2;3,17) and w(2;3,18)
| journal = Integers
| volume = 10
| issue =4
| year = 2010
| pages = 369–377
| doi=10.1515/integ.2010.032
| mr = 2684128
| s2cid=124272560
}}
</ref><ref name=ahmed2011>
{{
cite journal
| last = Ahmed
| first=Tanbir
| title=On computation of exact van der Waerden numbers
| journal = Integers
| volume = 12
| year = 2012
| issue = 3
| pages = 417–425
| doi = 10.1515/integ.2011.112
| mr = 2955523
| s2cid=11811448
}}
</ref><ref name=ahmedJIS>
{{
cite journal
| last = Ahmed
| first = Tanbir
| title= Some More Van der Waerden numbers
| journal = Journal of Integer Sequences
| volume = 16
| issue = 4
| year = 2013
| pages = 13.4.4
| mr = 3056628
}}
</ref><ref name=aks2011>
{{
cite journal
| last1 = Ahmed
| first1=Tanbir
| last2 = Kullmann
| first2 = Oliver
| last3 = Snevily
| first3 = Hunter
| title= On the van der Waerden numbers w(2;3,t)
| arxiv = 1102.5433
| journal = [[Discrete Applied Mathematics]]
| volume = 174
| issue = 2014
| pages = 27–51
| doi = 10.1016/j.dam.2014.05.007 | doi-access = free
| mr = 3215454
| year=2014
}}
</ref> (between 2009 and 2014) computed several [[van der Waerden number]]s using [[DPLL algorithm]]-based stand-alone and [[distributed SAT-solver]]s. Ahmed first used cluster-distributed [[SAT-solver]]s to prove w(2; 3, 17) = 279 and w(2; 3, 18) = 312 in 2010.<ref name=ahmed2010 /> 
* [[Optimal solutions for Rubik's Cube]] can be obtained in at most 20 face moves, 2010<ref>{{cite web |url=http://www.cube20.org/ |title=God's Number is 20 |website=cube20.org|date=July 2010|access-date= 2023-10-18}}</ref>
* Minimum number of clues for a solvable [[Sudoku|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.<ref>{{cite journal|last1=Cesare|first1=Chris|title=Maths whizz solves a master's riddle|journal=Nature|volume=526|issue=7571|pages=19–20|doi=10.1038/nature.2015.18441|pmid=26432222|date=1 October 2015|bibcode=2015Natur.526...19C|doi-access=free}}</ref>
* [[Boolean Pythagorean triples problem]] solved using 200 [[terabytes]] of data in May 2016.<ref>{{Cite journal|last = Lamb|first = Evelyn|date = 26 May 2016|title = Two-hundred-terabyte maths proof is largest ever|journal = Nature|doi = 10.1038/nature.2016.19990|volume=534|issue = 7605|pages=17–18|pmid=27251254|bibcode = 2016Natur.534...17L|doi-access = free}}</ref>
* Applications to the [[Kolmogorov-Arnold-Moser theorem|Kolmogorov-Arnold-Moser theory]]<ref>{{cite journal |last1=Celletti |first1=A. |last2=Chierchia |first2=L.  |title=Rigorous estimates for a computer-assisted KAM theory |journal=Journal of Mathematical Physics |volume=28 |issue=9 |pages=2078–86 |date=1987 |doi=10.1063/1.527418 |bibcode=1987JMP....28.2078C |url=https://aip.scitation.org/doi/abs/10.1063/1.527418}}</ref><ref>{{cite journal |last1=Figueras |first1=J.L. |last2=Haro |first2=A. |last3=Luque |first3=A. |title=Rigorous computer-assisted application of KAM theory: a modern approach |journal=Foundations of Computational Mathematics |volume=17 |issue=5 |pages=1123–93 |date=2017 |doi=10.1007/s10208-016-9339-3 |url=https://link.springer.com/article/10.1007/s10208-016-9339-3 |arxiv=1601.00084|hdl=2445/192693 |s2cid=28258285 }}</ref>
* [[Kazhdan's property (T)]] for the [[automorphism group of a free group]] of rank at least five
* [[Schur's theorem#Ramsey theory|Schur number five]], the proof that S(5) = 161 was announced in 2017 by [[Marijn Heule]] and took up 2 [[petabytes]] of space<ref>{{cite arXiv |last=Heule |first=Marijn J. H. |author-link=Marijn Heule|title=Schur Number Five |eprint=1711.08076 |date=2017 |class=cs.LO }}</ref><ref>{{Cite web|title=Schur Number Five|url=https://www.cs.utexas.edu/~marijn/Schur/|access-date=2021-10-06|website=www.cs.utexas.edu}}</ref>
* [[Keller's conjecture]] in dimension 7 the only remaining case in 2020 with a 200 [[gigabyte]] proof<ref>{{Cite book|last1=Brakensiek|first1=Joshua|last2=Heule|first2=Marijn|last3=Mackey|first3=John|last4=Narváez|first4=David|title=Automated Reasoning |chapter=The Resolution of Keller's Conjecture |date=2020|editor-last=Peltier|editor-first=Nicolas|editor2-last=Sofronie-Stokkermans|editor2-first=Viorica|series=Lecture Notes in Computer Science|volume=12166 |publisher=Springer |pages=48–65|doi=10.1007/978-3-030-51074-9_4|isbn=978-3-030-51074-9|pmc=7324133}}</ref><ref>{{Cite web|last=Hartnett|first=Kevin|date=2020-08-19|title=Computer Search Settles 90-Year-Old Math Problem|url=https://www.quantamagazine.org/computer-search-settles-90-year-old-math-problem-20200819/|access-date=2021-10-08|website=Quanta Magazine|language=en}}</ref>
* The packing chromatic number of the infinite square grid is 15, by Subercaseaux and [[Marijn Heule|Heule]] in 2023<ref>{{Cite arXiv |last1=Subercaseaux |first1=Bernardo |last2=Heule |first2=Marijn J. H. |date=2023-01-23 |title=The Packing Chromatic Number of the Infinite Square Grid is 15 |class=cs.DM |eprint=2301.09757 }}</ref><ref>{{Cite web |last=Hartnett |first=Kevin |date=2023-04-20 |title=The Number 15 Describes the Secret Limit of an Infinite Grid |url=https://www.quantamagazine.org/the-number-15-describes-the-secret-limit-of-an-infinite-grid-20230420/ |access-date=2023-04-20 |website=Quanta Magazine |language=en}}</ref> (See also: [[Hadwiger–Nelson problem]] for the chromatic number of the plane)}}

===Theorems for sale===
In 2010, academics at The [[University of Edinburgh]] offered people the chance to "buy their own theorem" created through a computer-assisted proof. This new theorem would be named after the purchaser.<ref>{{cite web|title=Herald Gazette article on buying your own theorem|url=http://www.heraldscotland.com/news/education/your-own-maths-theorem-for-15-1.1068654|work=Herald Gazette Scotland|date=November 2010|url-status=dead|archive-url=https://web.archive.org/web/20101121000707/http://www.heraldscotland.com/news/education/your-own-maths-theorem-for-15-1.1068654|archive-date=2010-11-21}}</ref><ref>{{cite web|title=School of Informatics, Univ.of Edinburgh website|url=http://www.ed.ac.uk/informatics/news-events/recentnews/theorem|work=School of Informatics, Univ.of Edinburgh|date=April 2015}}{{Dead link|date=July 2019 |bot=InternetArchiveBot |fix-attempted=yes }}</ref> This service now appears to no longer be available.

== See also ==
{{columns-list|colwidth=22em|
* [[Formal verification]]
* [[Logic Theorist]]
* [[Mathematical proof]]
* [[Metamath]]
* [[Model checking]]
* [[Seventeen or Bust]]
* [[Symbolic computation]]
* [[Validated numerics]]
}}

==References==
{{reflist|2}}

==Further reading==
*{{cite thesis |author-link=Douglas Lenat |first=D.B. |last=Lenat |title=AM: An artificial intelligence approach to discovery in mathematics as heuristic search |date=1976 |type=PhD |publisher=AI Lab., Stanford University |url=https://apps.dtic.mil/sti/pdfs/ADA155378.pdf |id=STAN-CS-76-570, Heuristic Programming Project Report HPP-76-8}}
*{{cite book |editor1-last=Meyer |editor1-first=K.R. |editor2-last=Schmidt |editor2-first=D.S. |title=Computer aided proofs in analysis |publisher=Springer |series=IMA volumes in mathematics and its applications |volume=28 |date=2012 |isbn=978-1-4613-9092-3 |url={{GBurl|JzLrBwAAQBAJ|pg=PP12}}}}
*{{cite book |last1=Nakao |first1=M. |first2=M. |last2=Plum |first3=Y. |last3=Watanabe |title=Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations |publisher=Springer  |series=Springer Series in Computational Mathematics |date=2019 |isbn=9789811376696 |url={{GBurl|Xrm9DwAAQBAJ|pg=PR7}}}}

==External links==
*{{cite journal |first=Oscar E. |last=Lanford |title=A computer-assisted proof of the Feigenbaum conjectures |journal=Bull. Amer. Math. Soc. |volume=6 |issue=3 |pages=427–434 |date=1982 |doi= 10.1090/S0273-0979-1982-15008-X|url=https://www.ams.org/journals/bull/1982-06-03/S0273-0979-1982-15008-X/S0273-0979-1982-15008-X.pdf |citeseerx=10.1.1.434.8389 }}
*{{cite tech report |first=Edmund |last=Furse |title=Why did AM run out of steam? |date=1990 |id=CS-90-4 |publisher=Department of Computer Studies, University of Glamorgan |url=https://www.comp.glam.ac.uk/pages/staff/efurse/Abstracts/Why-did-AM-halt.html |access-date=2016-09-06 |archive-date=2012-07-17 |archive-url=https://web.archive.org/web/20120717094035/https://www.comp.glam.ac.uk/pages/staff/efurse/Abstracts/Why-did-AM-halt.html |url-status=bot: unknown }}
*{{cite news |first=S. |last=Begley |title=Number proofs done by computer might err |newspaper=Pittsburgh Post-Gazette |date=April 16, 2018 |url=http://www.post-gazette.com/businessnews/2007/01/12/Number-proofs-done-by-computer-might-err/stories/200701120255|archive-url=https://web.archive.org/web/20180416201308/http://www.post-gazette.com/businessnews/2007/01/12/Number-proofs-done-by-computer-might-err/stories/200701120255 |archive-date=2018-04-16 }}
* {{cite web|title=A Special Issue on Formal Proof|url=https://www.ams.org/notices/200811/|work=Notices of the [[American Mathematical Society]]|date=December 2008}}

{{Mathematical logic}}
{{Numerical PDE}}

[[Category:Argument technology]]
[[Category:Automated theorem proving]]
[[Category:Computer-assisted proofs]]
[[Category:Formal methods]]
[[Category:Numerical analysis]]
[[Category:Philosophy of mathematics]]