2026-10-30
Hupyy's LPM checks 38,661,140 SAT leaves with cake_lpr. Under a stated trust base, Lean gives w(2;3,21)=416. No one outside the team has replayed every leaf.
The mixed van der Waerden number w(2;3,t) is the smallest n such that every red-blue colouring of 1 through n contains a red 3-term arithmetic progression or a blue progression of length t. For t=21, Kullmann in 2010 proved w(2;3,21) ≥ 416 and conjectured equality. Ahmed, Kullmann and Snevily in 2014 printed a valid colouring of 1 through 415, restated the conjecture, and wrote that settling it with similar resources seemed to need a new algorithmic idea. Exact values in the primary texts this paper read reach t=19: w(2;3,19)=349, from about 196 CPU-years, with resolution proofs discussed and no separately checkable upper-bound certificate in the report. The value 389 at t=20 is attributed to a 2015 chapter by Kouřil. This paper did not obtain that chapter, so whether a certificate exists there is unknown.
On 22 September 2026 Google DeepMind's Formal Conjectures benchmark tagged W(3,21)=416 as research open. The tag was still present in the 28 October 2026 commit.
Enumerating colourings is impossible. There are 2^416 red-blue colourings of 1 through 416, a number with 126 decimal digits. The argument encodes the claim as a propositional formula and refutes it case by case.
F(3,21;416) has 416 variables and 47,176 clauses: 43,056 forbid a red triple and 4,120 forbid a blue 21-term progression. The formula is satisfiable exactly when a valid colouring exists. Lean proves that equivalence.
The split runs from the centre outward. Position i is paired with its mirror n+1−i, and the pairs are ordered by distance from the centre. Case j forces every inner pair to match its mirror, and forces pair j to disagree, red on the left and blue on the right. One palindromic case forces every pair to match. That is 209 cases. The clause set is closed under reversal, and Lean proves that a satisfiable formula meets at least one of these cases. Swapping colours is not a symmetry, because the two colours obey different rules. The split does not restrict the search to palindromes.
Each case is then cut by cube-and-conquer: a look-ahead solver picks partial assignments, and each one is refuted. A planner sizes the cuts by random dives, aiming at about 400 million estimated nodes per item. The driver probes each child with 500 random dives, cuts again above an estimate of 2.5 million nodes, and cuts again when a proof passes 4 million lemmas, to depth 5. A modified tawSolver emits LRAT. The proof is piped into cakelpr and never stored. cakelpr is the LRAT checker of Tan, Heule and Myreen, verified in CakeML. A leaf counts only when the checker's entire output is the single line s VERIFIED UNSAT. The checker exits 0 when it refuses a proof, so the exit code is recorded and not trusted.
Sixteen cases are two-level covers, c001 through c015 and c018, holding 235,314 items. The other 193 are flat. A composition theorem turns "the cubes cover the case" and "every leaf is unsatisfiable" into the claim that no colouring of 1 through 416 is valid. The lower bound is the 2014 colouring of 1 through 415, accepted by Lean's decide inside the kernel. From those hypotheses the theorem gives IsW 21 416, which is w(2;3,21)=416. The same pipeline gives IsW 20 389.
LPM, described as a scalable neuro-symbolic system, produced the pipeline. Its agents wrote the Lean 4 development and ran the computation on AWS. Commit records name Claude Fable 5.1, Claude Opus 5.5, Claude Opus 5, Codex and Codex GPT-6 as co-authors of the commits. Only steps the Lean kernel accepted, and refutations cakelpr accepted, enter the result. Printers, digest comparison and the binder sit outside both checkers and are trusted. The prose is not machine-checked.
The final statement depends only on the axioms propext and Quot.sound. No classical choice, and no native-evaluation axiom. Native evaluation runs compiled code in place of a kernel check and admits the result as an axiom. Szeider's Lean proofs of w(2;3,17)=279 and w(2;3,18)=312 use that route. Here the verdicts on 38,661,140 leaves stay hypotheses of the theorem.
| Quantity | t=21 | t=20 |
| Claim under the trust base | w(2;3,21)=416 | w(2;3,20)=389 |
| Cases bound | 209 | 195 |
| Completed leaves | 38,661,140 | 5,244,544 |
| Process CPU-hours | 390,516.0 | 29,646.9 solving, 10,942.9 leaf checks |
| Certificate stream, not stored | 5,069,860,346,325,430 bytes | 594,078,127,187,870 bytes |
Of the 390,516.0 hours at t=21, solving with proof emission took 279,602.4 and leaf checking took 104,298.4. Production used 870 machines of 24 Graviton4 types and 449,427.374 vCPU-hours. Per leaf, process CPU is 22.2 seconds at the median, 114.5 at the 95th percentile and 433.0 at the maximum. The median search-node count is 422,589.
A second program, written without the binder's code, re-derived every cover at t=21 from the raw records. For all 209 cases the cube list matches the accepted leaves, all 38,661,140 of them, each with an accepted verdict, and none missing, extra or duplicated. All 235,523 cover digests used by the Lean hypotheses reprint byte-for-byte from those leaves.
A seeded sample re-solved 30,000 leaves across all 209 cases. All 30,000 matched the recorded formula digest, checker line, and node and lemma counts, in 292.2 process CPU-hours and 1.7 hours of wall time on one c8g.metal-48xl. If each record were independently wrong with probability at least 0.0001, a sample of this size would contain a bad record with probability at least 95 percent. The matching one-sided 95 percent upper bound on the per-record error rate is about 0.00009985. The bound does not cover defects that are clustered or planted.
Alexander Fedin, at Hupyy, took no part in the computation, the formalisation or the writing. All 1,899 files in the package matched SHA256SUMS, the axiom list of all 458 theorems matched the shipped list, and the main theorem depends only on propext and Quot.sound. With his own build of cakelpr he replayed c080 at t=20, 8 leaves and 246,152 nodes, and c074 at t=21, 11 leaves, 1,392,315 nodes, 83.6 seconds. He states the limit: one case out of 209, run by a reviewer on the authors' package, not a full independent replay. His Lean build reported PARTIAL, because the release package does not ship the manuscript and three manuscript checks did not apply.
The Boolean Pythagorean triples computation used about 35,000 CPU-hours of cubing and solving and almost 200 TB of DRAT proofs, and those proofs were kept. The certificate stream here is about 5,070 TB, roughly 25 times that volume, and it is discarded after checking. The paper claims neither a new algorithm nor a speed-up. The t=20 result is a certificate-backed check of the value attributed to Kouřil, with no claim of first exactness or first certification.
The 2010 conjecture was still tagged as open research on DeepMind's Formal Conjectures list at the end of October 2026. If the trust base in Section III.F holds, w(2;3,21)=416 comes off that list, and w(2;3,20)=389 gains a per-leaf check the sources this paper could read did not supply.
The contribution is the shape of the evidence, not a faster SAT solver. A Lean theorem whose hypotheses are finite files, every refutation read by cakelpr, no proof stored, every file tied by SHA-256 to the Lean term it was printed from. Using the result means using the replay package. The companion Zenodo deposit holds the Lean sources, the delivered set of all 209 cases and the per-leaf records. Rechecking one leaf means regenerating its proof with the command in that package. The dollar cost is not reported.
The equality is not closed inside the Lean kernel. The encoding, the centre-out split, the composition and the colouring of 1 through 415 are kernel proofs. Unsatisfiability of the 38.7 million leaves is a cakelpr record from outside the kernel. An earlier route imported one 85-literal sub-leaf into the kernel: five completed modules took 85,721 seconds and peaked at 18.39 GiB. Whether a computation of this size can be checked inside the kernel is left open.
Proofs are not retained, so a recheck means solving again. Solving plus leaf checking on the production run took 383,900.8 process CPU-hours. A full replay is another computation of that size.
No full recheck exists outside the producing team or outside Hupyy. The t=20 replay described as non-author was an automated agent of the producing team that had not produced the cases. It covered 184 of 195 cases, which hold 5.5 percent of the leaves, and it re-solved only the three smallest leaves of each row plus the unit-refuted leaves. The other verdicts were trusted as recorded. The sample of 30,000 leaves is about 0.08 percent of 38,661,140.
Negative controls show that this checker build refuses mutated certificates. They do not re-prove soundness at this scale. That still rests on the published CakeML verification. The assembly is trusted as the upstream repository released it, and the paper does not claim it equals CakeML's compiled output. Leaves that were not printed through Lean also trust the compiled printer and Python's decimal rendering of integers. A shared bug there is invisible to the digest check. The kit's path for a two-level cover has not been run from the package on a two-level case. Whether w(2;3,22) is in reach is not discussed. The author, Eitan Nahmias, is affiliated with Hupyy, which develops LPM. Fedin is at Hupyy as well.