Content deleted Content added
→References: see also |
Approximation for scale |
||
Line 6:
{{math theorem| The set {1, . . . , 7824} can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for {1, . . . , 7825}.<ref name="arXiv"/>}}
There are {{nowrap|2<sup>7825</sup> ≈ 3.63×10<sup>2355</sup>}} colorings for the numbers up to [[7825 (number)|7825]]. These possible colorings were logically and algorithmically narrowed down to around a trillion (still highly complex) cases, and those were examined using a [[Boolean satisfiability]] solver. Creating the proof took about 4 years of CPU time over two days on the Stampede supercomputer at the [[Texas Advanced Computing Center]] and generated a 200 terabyte propositional proof, which was compressed to 68 gigabytes.
The paper describing the proof was published on [[arXiv]] on 3 May 2016,<ref name="arXiv">{{Cite journal|last=Heule|first=Marijn J. H.|last2=Kullmann|first2=Oliver|last3=Marek|first3=Victor W.|date=2016-05-03|title=Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer |arxiv=1605.00723|doi=10.1007/978-3-319-40970-2_15|journal=Lecture Notes in Computer Science|pages=228–245}}</ref> and has been accepted for the SAT 2016 conference, where it won the best paper award.<ref>[http://sat2016.labri.fr/ SAT 2016]</ref>
| |||