The problem
Is there a 2-colouring of \mathbb{N} (equivalently of {1,…,N} for all N) such that no Pythagorean triple (a² + b² = c²) is monochromatic? Answer: NO — every colouring fails by N = 7825, while {1,…,7824} admits valid colourings.
The Boolean Pythagorean Triples Problem
historicReferences
History & significance
Ronald Graham offered $100 for the answer in the 1980s, a question rooted in Schur-type partition regularity (Pythagorean triples are not partition regular — unlike Schur triples). Human techniques were hopeless: the statement quantifies over all colourings of infinitely constrained structure.
The resolution (computer-assisted proof)
Resolved May 2016 by Marijn Heule, Oliver Kullmann and Victor Marek: massive SAT encoding + Cube-and-Conquer decomposition (one million subproblems) solved by the Stampede supercomputer (~2 days, 800 cores), producing a 200 TB DRAT certificate — mechanically verified end-to-end, and compressed losslessly to 68 GB via symmetry-aware trimming. Published in Nature as a landmark of formalised extreme-scale reasoning. Graham's cheque went to Heule. The number 7825 entered the mathematical permanent record.