The 200-Terabyte Proof: How Computers Solved a Coloring Puzzle Too Large for Humans to Check
A Simple Coloring Puzzle With a Giant Answer
In 2016, Marijn Heule, Oliver Kullmann, and Victor Marek used computers to settle the Boolean Pythagorean triples problem. They proved that the numbers 1 through 7,824 can be colored red or blue without creating a one-color Pythagorean triple—but adding 7,825 makes such a coloring impossible. The resulting proof occupied almost 200 terabytes.
The puzzle begins with a familiar equation:
a² + b² = c²
When three positive whole numbers satisfy this equation, they form a Pythagorean triple. The best-known example is 3, 4, and 5:
3² + 4² = 9 + 16 = 25 = 5²
Now imagine coloring every positive integer either red or blue. The challenge is to avoid coloring all three members of any Pythagorean triple the same color.
If 3 and 4 are red, for example, then 5 must be blue. If 5 and 12 are blue, then 13 must be red. Every new triple adds another restriction, and many numbers belong to several different triples.
The big question was deceptively simple: Could this coloring continue forever?
The answer is no—but proving that required one of the largest computer-generated proofs ever created.
The Remarkable Boundary at 7,825
For a while, it appears that clever coloring might always succeed. The researchers found that every number from 1 through 7,824 can indeed be assigned one of two colors without producing a completely red or completely blue Pythagorean triple.
Then comes 7,825.
Once the numbers 1 through 7,825 are included, there is no successful coloring. No matter how the two colors are assigned, at least one Pythagorean triple will be entirely red or entirely blue. This made 7,825 the exact breaking point.
This distinction is important because the proof had two parts:
- Existence: Show at least one valid coloring for 1 through 7,824.
- Impossibility: Show that no valid coloring exists for 1 through 7,825.
The first task can be completed by presenting a successful coloring and checking its triples. The second is much harder. Finding millions of failed colorings would prove nothing, because one undiscovered successful arrangement might still exist.
To establish impossibility, the researchers had to rule out every possible coloring.
Why Ordinary Brute Force Could Never Work
Each of the 7,825 numbers has two color choices. That creates:
2⁷⁸²⁵ possible colorings
This is approximately 3.63 × 10²³⁵⁵—a number containing 2,356 decimal digits. Testing that many arrangements one at a time would be hopeless, even with extremely fast machines.
Fortunately, the computers did not blindly examine every coloring. They used logic to eliminate enormous groups of possibilities together.
Suppose a partial coloring makes 3 and 4 red. There is no need to explore any continuation in which 5 is also red. That entire branch can immediately be rejected. Similar deductions ripple through thousands of overlapping triples.
This resembles backtracking, a technique also seen in the Eight Queens Puzzle and its 92 solutions. A solver makes choices, follows their consequences, and abandons a branch as soon as it becomes impossible.
The difference is scale. Eight Queens fits on a chessboard. The Pythagorean problem formed a vast web of numerical relationships extending across thousands of integers.
Turning the Puzzle Into SAT
The breakthrough came from translating the coloring challenge into a Boolean satisfiability problem, usually called SAT.
In Boolean logic, every variable has one of two values: true or false. Here, each number became a variable, with the two truth values representing red and blue.
For every Pythagorean triple, the researchers added rules saying:
- The three numbers cannot all be red.
- The three numbers cannot all be blue.
For 3, 4, and 5, the encoded formula therefore rejected the two forbidden color patterns while allowing the other six.
A SAT solver searches for values that satisfy every rule simultaneously. If it finds them, the formula is satisfiable, meaning a valid coloring exists. If it proves that no assignment can satisfy all the rules, the formula is unsatisfiable.
The formula for 1 through 7,824 was satisfiable. The one for 1 through 7,825 was not. The researchers describe the complete encoding and method in their published Boolean Pythagorean triples paper.
How Cube-and-Conquer Divided the Impossible
Even advanced SAT software needed help managing a problem of this size. The team used a method called Cube-and-Conquer, which combines two styles of automated reasoning.
The Cube Stage
First, a look-ahead program selected useful decisions and divided the original problem into many smaller subproblems called cubes.
Imagine an enormous maze. Instead of sending one explorer into it, you divide the maze into sections and assign each section to a different explorer. Together, the sections still cover every possible route.
The Conquer Stage
A second kind of SAT solver then attacked each cube. These programs learned from contradictions, allowing them to avoid repeating similar mistakes.
If every cube ended in contradiction, the original problem had no solution. The workload could also be distributed across many processor cores, making parallel computing especially valuable.
Using approximately 800 cores on the Stampede supercomputer, the main calculation took about two days. The project’s official proof and data page preserves the explanation, encodings, tools, and reconstruction resources.
This approach did more than search quickly. It produced a record of why all possible branches failed.
What Was Inside the 200-Terabyte Proof?
The proof was not a 200-terabyte essay filled with ordinary mathematical sentences. It was a gigantic formal log containing machine-readable deductions.
Its format, known as DRAT, allowed a separate proof-checking program to confirm that the SAT solver’s conclusion followed logically from the encoded rules. The full reconstructed proof was almost 200 terabytes, while the researchers released a compressed 68-gigabyte certificate from which it could be rebuilt.
A human could understand the original question, inspect the encoding, study the algorithms, and examine the checking software. What no human could realistically do was read and verify every line of the complete proof record manually.
That is why the checker mattered. Rather than simply trusting a solver that announced “no solution,” researchers could use software to validate the deduction trail. Contemporary reports noted that reconstructing and checking the certificate still demanded tens of thousands of processor hours.
The 200-terabyte figure therefore represents audit information, not mathematical decoration. The computer was effectively keeping an extraordinarily detailed record of its reasoning.
Can a Proof Count If Humans Cannot Read It?
Computer-assisted proofs raise a fascinating philosophical question: if no person can personally inspect every step, is the result truly understood?
This debate did not begin in 2016. The 1976 proof of the Four Color Theorem also relied on computer checks, causing mathematicians to reconsider what a proof could look like. You can explore that earlier milestone in the story of the map-coloring puzzle that took 124 years to solve.
A traditional proof ideally provides both certainty and insight. It explains not only that something is true, but often why it must be true.
The Pythagorean triples proof provides powerful formal evidence, but it does not reveal a short, elegant reason that 7,825 is the critical number. The impossibility emerges from a huge collection of interacting constraints rather than one memorable trick. As a detailed CNRS explanation of the computation noted, separate software was used to verify the enormous result.
What This Achievement Teaches Us About Puzzles
The 200-terabyte proof shows that a puzzle can be easy to state yet unimaginably difficult to settle. Its importance goes beyond one unusual coloring challenge.
It demonstrates how computers can:
- Translate playful questions into formal logic
- Divide enormous searches into manageable pieces
- Reject whole families of impossible choices
- Record deductions in a checkable format
- Prove that no hidden solution remains
Similar ideas appear in scheduling, circuit verification, software testing, and mathematical research. They also help explain how computers can establish negative results, such as proving that a smaller construction cannot exist. The 17-clue Sudoku challenge offers another accessible example: finding a sparse Sudoku was one challenge, but proving that no 16-clue version could have a unique solution was a much deeper one.
Most importantly, the Boolean Pythagorean triples problem was not solved by raw speed alone. Human researchers chose the representation, designed the algorithms, identified useful symmetries, organized the computation, and created ways to check the output.
The computer handled a scale of reasoning no person could manage line by line. Human mathematical insight made that computation meaningful.
A New Kind of Mathematical Feat
The final answer can be stated in one sentence: Two colors can safely cover the integers through 7,824, but not through 7,825.
Behind that compact result lies a 200-terabyte mountain of formal deductions.
That contrast is what makes the achievement so memorable. A question involving two colors and a schoolroom equation became a landmark in automated reasoning. It showed that computers can do more than find promising patterns or calculate large numbers—they can help establish mathematical impossibility.
The proof may be too large for any human to read from beginning to end, but its lesson is wonderfully clear: sometimes a tiny puzzle opens the door to an entirely new way of proving what is true.
