Boolean Pythagorean triples problem: Difference between revisions

Revision as of 23:02, 5 January 2025

Latest revision as of 06:30, 6 July 2025

(3 intermediate revisions by 2 users not shown)

Line 1:

{{short description|Can one split the integers into two sets such that every Pythagorean triple spans both?}}

The '''Boolean Pythagorean triples problem''' is a problem from [[Ramsey theory]] about whether the [[natural number|positive integers]] can be colored red and blue so that no [[Pythagorean triple]]s consist of all red or all blue members. The Boolean Pythagorean triples problem was solved by [[Marijn Heule]], Oliver Kullmann and [[Victor W. Marek]] in May 2016 through a [[computer-assisted proof]], which showed that such a coloring is only possible up to the number 7824.<ref name="nature">{{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>

==Statement==

Line 8:

==Solution==

[[Marijn Heule]], Oliver Kullmann and Victor W. Marek showed that such a coloring is only possible up to the number 7824. The actual statement of the theorem proved is

Marijn Heule, Oliver Kullmann, and Victor W. Marek demonstrated that it is possible to partition the set <math>\{1, \ldots, 7824\}</math> into two subsets such that neither subset contains a Pythagorean triple. However, such a partition is not possible for the set <math>\{1, \ldots, 7825\}</math>. This result was achieved by analyzing a vast number of possible colorings, which initially amounted to about <math>2^{7825}</math> combinations.The researchers reduced this to around a trillion cases, which were then tested using a SAT solver. The computational process required approximately 4 CPU-years over two days on the Stampede supercomputer at the Texas Advanced Computing Center. The resulting proof, initially 200 terabytes in size, was compressed to 68 gigabytes.The findings were published in the SAT 2016 conference paper "Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer," which received the best paper award.

{{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⁷⁸²⁵ ≈ 3.63×10²³⁵⁵}} possible coloring combinations 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, expressed as [[Boolean satisfiability]] problems, were examined using a [[SAT solver]]. Creating the proof took about 4 CPU-years of computation over a period of 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 in the SAT 2016 conference,<ref name="arXiv">{{Cite conference|last1=Heule|first1=Marijn J. H.|last2=Kullmann|first2=Oliver|last3=Marek|first3=Victor W.|author3-link=Victor W. Marek|year=2016|contribution=Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer |arxiv=1605.00723|doi=10.1007/978-3-319-40970-2_15|series=Lecture Notes in Computer Science|volume=9710|pages=228–245|title=Theory and Applications of Satisfiability Testing – SAT 2016: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings|editor1-first=Nadia|editor1-last=Creignou|editor2-first=Daniel|editor2-last=Le Berre}}</ref> where it won the best paper award.<ref>[http://sat2016.labri.fr/ SAT 2016]</ref> The figure below shows a possible family of colorings for the set {1,...,7824} with no monochromatic Pythagorean triple, and the white squares can be colored either red or blue while still satisfying this condition.

[[File:Ptn-7824-zoom-2.png|alt=|center|400x400px]]

==Prize==