The problem 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 <math>a^2+b^2=c^2</math> are all the same color.
For example, in the Pythagorean triple 3, 4 and 5 (<math>3^2+4^2=5^2</math>), if 3 and 4 are colored red, then 5 must be colored blue.
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
Шаблон:Math theorem
There are Шаблон:Nowrap possible coloring combinations 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, 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,[2] where it won the best paper award.[3] 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.
Prize
In the 1980s Ronald Graham offered a $100 prize for the solution of the problem, which has now been awarded to Marijn Heule.[1]
Generalizations
As of 2018, the problem is still open for more than 2 colors, that is, if there exists a k-coloring (k ≥ 3) of the positive integers such that no Pythagorean triples are the same color.[4]