Boolean Pythagorean triples problem
This problem is from Ramsey theory and asks if it is possible to color each of the positive integers either red or blue, so that no Pythagorean triple of integers a, b, c, satisfying are all the same color. For example, in the Pythagorean triple 3, 4 and 5 (), if 3 and 4 are colored red, then 5 must be colored blue.
Marijn Heule, Oliver Kullmann and Victor Marek investigated the problem, and showed that such a coloring is only possible up to the number 7824. The actual statement of the theorem proved is
There are 27825 ≈ 3.63×102355 colorings for the numbers up to 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 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.
- Lamb, Evelyn (26 May 2016). "Two-hundred-terabyte maths proof is largest ever". Nature. 534: 17–18. Bibcode:2016Natur.534...17L. doi:10.1038/nature.2016.19990. PMID 27251254.
- Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016-05-03). "Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer". Lecture Notes in Computer Science: 228–245. arXiv:1605.00723. doi:10.1007/978-3-319-40970-2_15.
- SAT 2016