Pattern · a proof you can operate but not read

The File That Said No

Colour every whole number from 1 to 7824 red or blue so that no Pythagorean triple ends up all one colour. It can be done, and the colouring is on this page: press the button and the browser regenerates all 9,465 triples and checks every one. Now try 7825. Nobody can do it, and the proof of that is not an argument. It is a file.

Ronald Graham asked the question, and offered a prize for the answer. The two sources date those two acts differently and neither dates the money: the authors' artifact page says the problem "was asked by Ronald Graham in the 1980s" and separately mentions "the $100 we got", while the 2016 abstract says only that "A prize for the solution was offered by Ronald Graham over two decades ago". In 2016 Marijn Heule, Oliver Kullmann and Victor Marek collected it. Their answer was a CNF formula fed through a SAT solver on 800 cores for about two days, which emitted a refutation trace their own paper describes as "almost 200 terabytes in size", out of which they extracted "a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking."

That is a strange kind of knowledge. It is certain, in a sense that a human argument almost never is, and it explains nothing. This page is an attempt to hold both halves at once. The small end of it you can operate completely. The large end you cannot, and the honest thing is to show you exactly where the handover happens.

Bench one · the tape

A colouring of 1 to 7824, and the check that it works

Below is a witness: one assignment of red or blue to each number from 1 to 7824. The grey cells are numbers that appear in no Pythagorean triple whose three members are all at most 7824, so within this tape they are genuinely unconstrained. Everything else is load bearing. Click any cell to flip that number, or type it into the box below the tape and press Flip it; the box is the keyboard route and does exactly the same thing.

The witness tape

1 to 7824, reading left to right, 96 per row

red blue in no triple with all members at most 7824 (free here) highlighted triple

Check only the prefix 1 to n 7824

Flip one number

Press Check all triples. The browser will generate every Pythagorean triple with c at most 7824 and test this colouring against all of them.

The tape is shipped as 7,824 bits of base64. Nothing else about it is taken on trust: the triples are generated here, from the definition, every time you press the button.

How tight is it? Of the 7,824 numbers, 4,260 cannot be flipped at all: change that one colour and a monochromatic triple appears immediately. 2,232 more sit in triples but have slack, and 1,332 appear in no Pythagorean triple whose three members are all at most 7824, so nothing on this tape constrains them. Read that last count carefully: 7313 is one of the 1,332, and it is not a number that appears in no triple. 2784² + 7313² = 7825². It is free only because the triple that catches it needs 7825, which this tape does not have. Those three counts are recomputed in your browser when this page loads.

What that button does and does not prove. A witness that survives the check proves one thing exactly: a good colouring of 1 to 7824 exists. Flip a number and you can destroy it in one click, which tells you how tight the arrangement is. But no amount of checking one colouring, or a thousand, can prove that every colouring of 1 to 7825 fails. That is the other direction, and it is the expensive one.

Bench two · the encoder

How a colouring problem becomes a logic formula

Give each number i a Boolean variable x_i: true means red, false means blue. A triple (a, b, c) is forbidden from being all red and forbidden from being all blue. That is exactly two clauses:

Triple to clauses

two clauses per triple, no encoding tricks

Triple index (sorted by c, then b) 1

loading…

The formula sizes, regenerated here

formula	triples	clauses	highest variable	published header	agrees

Be precise about what that right-hand column is. It is the DIMACS header line of each of the authors' published files, transcribed by hand into this page's source, and the browser compares its own freshly generated counts against that transcription. The browser makes no network requests and never sees the files themselves. What ties the transcription to the real files is the offline verifier: it parses research/boolean-pythagorean/vendor/*.cnf (pinned by SHA-256) and fails if any header row shipped here differs from the file.

Is the encoding faithful?

A SAT solver answering "unsatisfiable" is worth nothing if the clauses say something other than the mathematics. So: for a small prefix, count the colourings with no monochromatic triple by looking at triples directly, then count the assignments satisfying the clause set, by two separate pieces of code. They must agree exactly.

Exhaust all 2ⁿ colourings of 1 to n, with n = 16

Not run yet.

Vacuous settings are labelled, not hidden. Below n = 5 there is no Pythagorean triple at all, so "zero monochromatic triples" is true of every colouring and means nothing.

Bench three · the simplifier

The first thing the proof does is throw two thousand triples away

Before any search happens, the formula is shrunk. The technique is called blocked clause elimination, and in this problem it has a plain reading, which Cruz-Filipe and Schneider-Kamp spell out: remove from the list of triples every triple containing a number that occurs in no other triple. If a appears nowhere else, you can always fix a colouring of the rest by recolouring a at the end. Then iterate, because removing triples creates new lonely numbers.

Blocked clause elimination, run here

a fixpoint, not a heuristic

Not run yet.

What the browser compares here is the count: the surviving clause total against the transcribed header of the authors' published bce7825.cnf. The triple-for-triple set comparison against that file is real, but it is not running in this tab. It runs offline, in verify-boolean-pythagorean.mjs, which parses the pinned file and compares the two sets element by element.

Bench four · the checker

What a machine-checkable proof actually is

Here is the dismissal worth answering. An unreadable 200-terabyte file is just solver output. Why would anyone believe it? The answer is that the file is not the solver's reasoning. It is a sequence of clauses in a format called DRAT, and every line of it can be checked by a program much simpler and dumber than the solver that produced it. You can run that checker. It is below, written from scratch, on the authors' own worked example.

The example changes the equation from a² + b² = c² to a + b = c with a < b < c, because that one becomes impossible at 9 instead of 7825. It is an analogue, not a miniature of the real theorem, and the authors present it as such. But the proof format is identical, and the arithmetic of belief is identical.

The nine-variable refutation

a + b = c, a < b < c, on 1 to 9

Each box holds one line of the proof in DIMACS notation: a list of literals, positive for red, negative for blue. Edit any of them and check again. A line beginning with d is a deletion: it takes a clause back out of the formula instead of adding one.

Press Exhaust all 512 colourings to see that the formula really has no solution, then Check the proof.

The checker here implements RUP (reverse unit propagation) and RAT (resolution asymmetric tautology) on the first literal, which is what a DRAT checker does. It never asks the solver anything. Deletion lines are not checked at all, by design: taking a clause away can only make the empty clause harder to reach, never easier, so a deletion cannot launder a bad proof. It can, however, wreck a good one. The two buttons above insert one deletion each, immediately before the final line. One of them is harmless and one of them is fatal. The checker will tell you which.

The interesting part is which lines pass how. Line 1 is RUP: assume it false, propagate, hit a contradiction, done. That is ordinary resolution reasoning. Lines 2 and 3 are not RUP. They only pass the RAT test, which is a strictly stronger licence: it permits adding a clause that is not implied by the formula, as long as adding it cannot turn an unsatisfiable formula satisfiable. That single extra permission is why DRAT proofs can be written at all for problems this size, and it is the reason a 200-terabyte file is a proof rather than a log.

Bench five · the split

Cube and conquer: how one impossible problem becomes a million easy ones

The paper's title names the method, and nothing above has used it yet. Cube-and-conquer splits the formula into a set of cubes, each cube being a partial assignment, chosen so that every possible colouring falls under exactly one cube. Each cube is then handed to a solver as its own separate problem. If every cube is refuted, the formula is refuted, because the cubes leave nothing uncovered. The published run used a million top-level cubes and then split many of those again.

The interesting thing, and the reason the method works at all, is that the cubes are usually far easier than their sum. Below, the same nine-variable formula is split on its most frequently occurring variables. Watch the conquer phase disappear.

Split, then conquer

2^k cubes over the k most-occurring variables

Split depth k, the number of variables fixed in each cube 3

Not run yet.

Two honest differences from the real thing. The published split used a look-ahead heuristic that picks a different variable at each node and stops at a different depth on each branch, so its million cubes are not a uniform tree over one fixed variable list; and its conquer phase used a CDCL solver, not unit propagation and brute force. What transfers is the shape of the obligation: cover everything, refute each piece, and the coverage claim is the one you must not get wrong.

Bench six · the hinge

Where 7825 actually dies

Fix one number's colour to break the red-blue symmetry. Then some variables turn out to have the same value in every solution of the 7824 formula. That set is called the backbone, and the authors publish it: 2,304 variables, in the file backbone7824.cnf. Four of those numbers do the killing.

Before the bench, the one thing you have to hold on to, because the two published sources do not agree about it. Every clause in this encoding comes in a matched pair, one forbidding all red and one forbidding all blue, so the whole formula is unchanged when you swap the two colours. Swapping the colours of a solution therefore gives another solution, and swapping the colours of a backbone gives another backbone: the one belonging to the opposite symmetry break. So a backbone has two orientations, and only the choice of symmetry break picks one. What does not depend on that choice is the shape of the hinge: 5180 and 5865 share a colour, 625 and 7800 share the other colour, and those two colours are different. That is the part that kills 7825, and the bench separates it from the orientation.

The two identities that close it

recomputed here, colours read from the published backbone

Not run yet.

Squares and sums are computed here. The four colours are read from the authors' file, and that is the part this page does not reprove. The orientation of those colours is where the two sources part company, and the bench prints both.

Read this before you decide the hinge is the proof. Two square identities and four colours are a two-line argument. If that were the whole thing, nobody would have needed 800 cores. The expensive claim is the word every: that 5180 and 5865 take one colour, and 625 and 7800 the other, in every solution of the 7824 formula once the symmetry is broken. Establishing one such backbone fact means proving a formula of this size unsatisfiable, and there are 2,304 of them. The identities are the last inch of a very long road, and this page walks only that inch.

The two sources disagree about the orientation, and we are not going to hide it. The published backbone7824.cnf contains the unit clauses -5180, -5865, 625, 7800 and 2520, which under this page's convention (true means red) makes 5180 and 5865 blue, 625 and 7800 red, and the symmetry-broken variable 2520 red. Section 6.3 of Heule, Kullmann and Marek 2016 says the opposite for all four, verbatim: "variables x5180 and x5865 are both positive in the backbone, forcing x7825 to be negative due to 5180² + 5865² = 7825². At the same time, variables x625 and x7800 are both negative in the backbone forcing x7825 to be positive due to 625² + 7800² = 7825²." Those four polarities are exactly the file's, globally swapped. Take the file at its word and that makes them the backbone of the other symmetry break, the one that fixes 2520 to blue rather than red: not a contradiction about the mathematics but a different choice of orientation. The bench above checks the step that licenses that reading, namely that the formula really is closed under the swap. What the bench cannot do is tell you which of the two documents has the authors' intended orientation, because both orientations describe a genuine backbone. What we cannot reconcile is the paper with itself. Its Section 5.2 says the symmetry break assigns the chosen variable to true, and Cruz-Filipe and Schneider-Kamp record that "2520 was assigned to true"; under that convention Section 6.3's four signs and the published file cannot both be right. We have not resolved which is the slip, and we do not know. The page takes its orientation from the file, because the file is the object our witness was checked against, and it says so wherever an orientation is printed.

The scale

From four lines to almost two hundred terabytes

Everything above runs in this tab, but "instantly" would be a boast rather than a measurement, so here is the measurement, taken on your machine as this page loaded: the triple sweep and the tightness count that run on load took (measuring). The heaviest optional bench, the n = 22 census, costs roughly the same again on the desktop this was built on, and a phone is several times slower than a desktop. Nothing here is free; it is just small. Here is the same set of obligations at the size the real problem imposes. Left column: what this page actually did. Right column: what the published proof did, with the source for each figure.

obligation	here, live	in the published proof	source

Two of those numbers are constantly confused, so they are worth separating flatly. The almost 200 terabytes is the DRAT proof trace itself. The 68 gigabytes is a compressed certificate from which that trace can be reconstructed for checking. They are different objects, and the paper's own sentence puts them in that relation: the certificate was extracted from the proof so that anyone could rebuild it. We do not quote a compression ratio, because the source does not say whether its terabytes and gigabytes are powers of ten or powers of two. Read both units on the same convention, which is the only defensible reading, and "how many times smaller" comes out between 2,941 (decimal throughout) and 3,012 (binary throughout). Allow the terabytes and the gigabytes to be read on different conventions and the span widens to 2,739 at the bottom and 3,234 at the top. All four are divided out in your browser from the numbers 200 and 68 and rounded to a whole number. We decline to pick one of them, and no single figure on this page is a compression ratio.

The trust chain did not stop there. Luís Cruz-Filipe and Peter Schneider-Kamp formalised the argument in Coq. Their LPAR-21 paper, which is the version we read in full, connects the mathematical statement to the propositional formula, formalises the simplification step and the cube-and-conquer argument, and reduces the remaining obligation to checking the unsatisfiability of 1,000,001 formulas: the million cubes plus one formula asserting that no cube applies. That figure is theirs, read from their paper and cited, not recomputed anywhere on this page, which is why it does not appear in the ledger below. A journal version with Joao Marques-Silva as a third author appeared in 2019; we cite that one for the existence and scope of the formalisation only, because we did not obtain its full text. The conference paper is blunt about the residue. The proof data from the 2016 run is used as an untrusted oracle and re-checked; and a single Coq program that did the whole job end to end would, they write, "require several years on state-of-the-art hardware, which is clearly unfeasible."

The check

Running the checks…

quantity	shipped in this page	recomputed in your browser

Every uncertainty and free choice on this page.

Not proved here: the 7825 theorem. This page proves that a good colouring of 1 to 7824 exists, by exhibiting one and checking it. It does not replay the 68-gigabyte certificate and it does not establish that 1 to 7825 is impossible. For that it cites Heule, Kullmann and Marek (2016) and the Coq verification of Cruz-Filipe, Marques-Silva and Schneider-Kamp (2019).
Not proved here: the backbone. The 2,304 backbone literals are read from the authors' published backbone7824.cnf. We check that our witness agrees with all of them, and that check is weaker than it looks: the witness was produced by handing a solver that same file, units included, so the agreement is guaranteed by construction. What it tests is that the base64 blob shipped here decodes to the literals the solver was given, not that those literals are a backbone. We attempted one backbone bit ourselves with a modern CDCL solver and report the outcome in the research notes; it did not finish, and nothing about backbone-ness is settled in this page.
Unresolved: which orientation of the backbone is the published one. The file and Section 6.3 of the 2016 paper state the four hinge polarities opposite ways round, and the paper's own Section 5.2 convention agrees with the file rather than with its own Section 6.3. The caveat above quotes both. The page follows the file. Nothing else on the page depends on the choice, because the encoding is symmetric under swapping the colours and the bench checks that it is.
Free choice: which witness. The 7824 colouring shipped here is not canonical, and the authors do not publish one plain-text extremal colouring on their artifact page. Ours was found on 2026-07-31 with CaDiCaL 1.5.3 through PySAT, seeded with the published backbone units to make the search cheap. The same solver, given the formula without that hint, had not returned after twenty-three minutes on one core, which is why the hint is there. How it was found does not matter to the check: it is re-tested from scratch above. Any colouring that passes would do equally well; there are many.
Free choice: the tape geometry. 96 cells per row is chosen because it makes the structure legible, not because 96 means anything.
Free choice: the exhaustive census bound. The default n = 16 is a speed compromise. Nothing changes at 22 except the running time.
A global swap of red and blue is not evidence. Every clause in this encoding is symmetric under it by construction, so a flipped copy of a valid colouring is automatically valid and tells you nothing new. That is exactly why the authors fix one variable before computing a backbone at all.
Rounded quantities. "Almost 200 terabytes", "68 gigabytes", "800 cores" and "about 2 days" are the paper's own words and are rounded there. We do not sharpen them.
The superlative is dated and attributed. The authors' artifact page called this "the largest math proof ever" in 2016. The paper itself claims no superlative, only the measured size. We make no claim about what the largest proof is today.
Nothing here is new. Every result on this page is published. The reproductions (triple generation, the elimination fixpoint, the 512-assignment census, the DRAT check) are reimplementations, offered as checks, not as discoveries.

Offline mirror, run before publication: node research/boolean-pythagorean/verify-boolean-pythagorean.mjs. It regenerates the triples by two independent methods, parses this page's shipped numbers out of the HTML, and fails if any of them disagrees. It also parses the pinned CNF files themselves, compares the surviving triple set of the elimination against bce7825.cnf element by element, checks that every number written into the prose above is a number some bench recomputes, and checks that this page still carries the sentence from the 2016 paper that contradicts it.

What this proof does not explain, and what people asked next

Why 7825? The published work exposes a mechanism (a backbone that forces four numbers, and two Pythagorean triples that then collide at 7825) but it does not supply a short conceptual reason for the cutoff sitting where it does. Nothing on this page should be read as saying 7825 is special in any way beyond being the first number at which the constraints run out.

Does it fail for every larger n as well? Yes, and that part is trivial: any colouring of 1 to n for n greater than 7825 restricts to a colouring of 1 to 7825, which must already contain a monochromatic triple. It does not follow, and we do not claim, that the failure for a larger n involves a triple containing n itself.

Is there a human-readable proof? Unknown to us. The 2016 paper raises the question and does not answer it. As of 31 July 2026 we did not find a published human-surveyable proof of the 7825 result, and that sentence is a statement about our search on that date, not a theorem about the literature.

Does the Coq work make it readable? No. It narrows what you have to trust (the encoding, the simplification, the cube split, the checker's soundness) but it still processes the same enormous external proof data with extracted code. Reducing trust and producing understanding are different goods, and only the first one was on offer.

Sources, with identifiers

Marijn J. H. Heule, Oliver Kullmann and Victor W. Marek, "Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer", Theory and Applications of Satisfiability Testing (SAT 2016), LNCS 9710, pages 228 to 245. DOI 10.1007/978-3-319-40970-2_15. Preprint arXiv:1605.00723, v1 submitted 3 May 2016. Source of: the 7824/7825 boundary, the encoding, cube-and-conquer, "almost 200 terabytes", "a compressed certificate of 68 gigabytes", 800 cores, about 2 days, the existence and size of the backbone, and the two hinge identities. Not the source of the four hinge polarities as this page prints them: Section 6.3 states them the other way round, the quotation is given in full in the caveat above, and the polarities printed here are read from backbone7824.cnf instead.
Marijn J. H. Heule, "Everything's Bigger in Texas", Boolean Pythagorean Triples artifact page, cs.utexas.edu/~marijn/ptn/, retrieved 31 July 2026. Source of: the published CNF encodings, the backbone file, the million-cube partition, the nine-variable proof example and its four DRAT lines, and the phrase "the largest math proof ever". The page carries no version marker, so every file we use is pinned by SHA-256 in the research folder.
Luís Cruz-Filipe, Joao Marques-Silva and Peter Schneider-Kamp, "Formally Verifying the Solution to the Boolean Pythagorean Triples Problem", Journal of Automated Reasoning 63(3), pages 695 to 722, 2019. DOI 10.1007/s10817-018-9490-4. The peer-reviewed formalisation.
Luís Cruz-Filipe and Peter Schneider-Kamp, "Formally Proving the Boolean Pythagorean Triples Conjecture", LPAR-21, EPiC Series in Computing 46, 2017, author copy. This is the version we read directly, and it is the source of the sentences quoted above: "2136 of the original 9472 triples can be ignored", the "3745 propositional variables actually used", the "1,000,001" derived formulas, and "require several years on state-of-the-art hardware, which is clearly unfeasible".