Boolean Pythagorean Triples

You already know Pythagorean triples: whole numbers where $a^2 + b^2 = c^2$, like $3, 4, 5$ or $5, 12, 13$. Now play a coloring game. Take the numbers $1, 2, 3, \dots, n$ and paint each one red or blue — any way you like. The single rule: no Pythagorean triple may be all one color. So you can never have $a$, $b$ and $c$ with $a^2+b^2=c^2$ all painted red, and never all blue.

For small $n$ this is easy. The triples are sparse, you have plenty of room, and almost any sensible coloring works. The question is whether your luck ever runs out: is there some $n$ where, no matter how cleverly you split the numbers into two colors, some Pythagorean triple is forced to be monochromatic?

That gap between "always colorable" and "impossible" turns out to land on a single, very specific number — and finding it took one of the most extreme computations in the history of mathematics.

Below are the numbers $1$ to $40$. Click any number to flip it between red and blue. Every time a Pythagorean triple $a^2+b^2=c^2$ ends up all one color, it lights up as a violation. Try to color all $40$ with zero violations — for this range it is comfortably possible.

<p class="hint">{{hint}}</p>
<div id="grid" class="grid"></div>
<div class="status" id="status">{{violations_init}}</div>
<div class="btns">
  <button id="solve" type="button">{{btn_solve}}</button>
  <button id="random" type="button" class="ghost">{{btn_random}}</button>
  <button id="reset" type="button" class="ghost">{{btn_reset}}</button>
</div>
<div class="triples" id="triples"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.grid { display: grid; grid-template-columns: repeat(10, 1fr); gap: 5px; margin: .4rem 0; }
.tile { aspect-ratio: 1; display: flex; align-items: center; justify-content: center;
        font: 700 14px ui-monospace, monospace; border-radius: 7px; cursor: pointer;
        user-select: none; transition: transform .08s, box-shadow .12s; }
.tile:hover { transform: translateY(-1px); }
.red  { background: #f6d4d8; color: #a31523; border: 1px solid #e7a9b1; }
.blue { background: #d3e0f7; color: #173f86; border: 1px solid #a9c2ec; }
.tile.bad { box-shadow: 0 0 0 3px #f4b400; animation: glow .9s ease-in-out infinite alternate; }
@keyframes glow { from { box-shadow: 0 0 0 2px #f4b400; } to { box-shadow: 0 0 0 4px #ffce4d; } }
.status { font-size: 1rem; font-weight: 700; margin: .6rem 0; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .6rem; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.triples { font: 600 12px ui-monospace, monospace; color: #b00020; min-height: 1.3em; }

// Code not found

Press Auto-solve and the computer searches for a clean two-coloring of this small range. Notice how the constraints interlock: fixing one number's color quietly forces others. Now imagine stretching the range to thousands of numbers, where millions of triples overlap — the same search is what a SAT solver had to conquer to settle the real question.

Here is the punchline. The numbers $1$ to $7824$ can be split into two colors with no monochromatic Pythagorean triple. At $7825$ it becomes impossible — and not by a hair. This was proved by Marijn Heule, Oliver Kullmann and Victor Marek in 2016.

• It is a finite search, but an astronomically large one. Coloring $7825$ numbers means $2^{7825}$ possible colorings — far more than the atoms in the observable universe. No one checks them one by one.
• It was settled with a SAT solver. Each number becomes a Boolean variable (red or blue); each Pythagorean triple becomes a pair of clauses forbidding "all red" and "all blue". The question "is there a valid coloring?" becomes a single giant satisfiability instance.
• The proof is about 200 terabytes. Using a technique called cube-and-conquer, the team split the problem into nearly a trillion cases and verified each, producing a certificate so large it set a record as the largest mathematical proof ever generated. A separate, independently trusted checker confirmed it.
• Status: solved. The answer is exact — $7824$ yes, $7825$ no — and machine-verified. Unlike open problems such as P vs NP, this question has a final, checkable answer.

The unease many mathematicians felt was philosophical: we know the answer, but no human can read the whole proof. We trust it the way we trust a verified computation, not the way we follow a clever argument by hand.

A coloring riddle about $7825$ might sound like recreational math, but the machinery behind it is everywhere serious computing meets certainty:

• SAT solving at scale: the same solvers that cracked this problem verify that microprocessors and aircraft software behave correctly, encoding "can this system ever reach a bad state?" as satisfiability.
• Verified proofs: the 200-terabyte certificate was checked by an independent, formally trusted program. That same idea — produce a proof a machine can re-verify — is reshaping how we trust large computations.
• Ramsey-type problems: "no matter how you split things, some structure is forced" appears in scheduling, network design and combinatorics; this is a flagship example of a computer settling one.
• Pushing hardware limits: the run consumed days on a supercomputer and stress-tested storage and verification tooling, driving advances in how massive computations are recorded and trusted.

Learn how this problem was cracked and you've seen the modern shape of hard combinatorics — encode into SAT, search with massive parallelism, and emit a certificate anyone can re-check.

Two colors, one simple rule, and a wall that stands at exactly $7825$. The Boolean Pythagorean triples problem is solved — settled in 2016 by Heule, Kullmann and Marek with a SAT solver and a proof so vast it filled around 200 terabytes, the largest ever produced.

It is a glimpse of mathematics in the computer age: an answer that is final and verifiable, yet too big for any person to hold in their head. The grids in the demo above are the human-scale shadow of that wall. Reach far enough and the room for two colors runs out — and only a machine could prove exactly when. For problems still open, like P vs NP, no such certificate exists yet.