Boolean Pythagorean triples problem

The Boolean Pythagorean triples problem is a problem relating to Pythagorean triples which was solved using a computer-assisted proof in May 2016.^[1]

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 ${\displaystyle a^{2}+b^{2}=c^{2}}$ are all the same color. For example, a coloring with a and b red and c blue is an admissible coloring, but all three blue would not be.

The proof shows that such a coloring is impossible. Up to the number 7824 it is possible to color the numbers such that all Pythagorean triples are admissible, but the proof shows that no such coloring can be extended to also color the number 7825. The actual statement of the theorem proved is

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}.^[2]

There are 2⁷⁸²⁵ colorings for the numbers up to 7825. These possible colorings were logically narrowed down to just under a trillion cases, and those were examined using a Boolean satisfiability solver. Creating the proof took two days of computer execution time on the Stampede supercomputer at the Texas Advanced Computing Center and generated 200 terabytes of data.

In the 1980s Ronald Graham offered a $100 prize for the solution of the problem, which has now been awarded to Marijn Heule. The paper describing the proof was published on arXiv on 3 May 2016^[2] and has been accepted for the SAT 2016 conference.

References

1. Lamb, Evelyn (26 May 2016). "Two-hundred-terabyte maths proof is largest ever". Nature. doi:10.1038/nature.2016.19990.
2. Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016-05-03). "Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer". arXiv:1605.00723 [cs].