MathRecords

Extending tracked combinatorial records by computation, in a form where nobody has to take the computation's word for it.

Five new terms have been established, in five different families of mixed van der Waerden numbers whose published lists had all stood since 2012: A217058(12) = 57, A217005(19) = 52, A217007(7) = 68, A217236(4) = 84 and A217059(9) = 74. Each ships a certificate you can check without running a solver.

The fifth was withheld for nearly two weeks, and the reason is worth keeping. A217059 a(9) = 74 was computed and cross-checked alongside the others, but the family gate that reproduces the published a(8) = 70 as an independent check on the method was started and killed without a verdict, so the term sat on disk marked withheld rather than claimed. The gate was run to completion on 2026-08-11 and passed: SAT at n = 69 with a verified witness, UNSAT at n = 70, both at j = 8, 978.8 s for the pair (vdw/validate_gate59.json). A verification step that was defined and then not finished does not get waived retroactively because the answer looks right.

The paper. Five new mixed van der Waerden numbers, with machine-checked upper bounds -- 14 pages -- is the write-up: the encoding, the certificates, and the cube-and-conquer refutations. All five upper bounds are reduced to checked proof objects: 23,851 per-cube DRAT proofs in total, every one replayed to s VERIFIED by drat-trim, each family with a composition proof that its cube set covers the whole assignment tree. LaTeX source.

The equal-target families were the hard ones and are worth a sentence. The cube generator dropped colour-permutation images, which is sound when you are searching -- some other prefix is the image -- but is not a refutation, so the per-cube proofs never covered those branches and [3,3] and [4,4] could not be certified at all. Taking colour symmetry out of the cube set fixes it. Measured, not argued: the cube sets are byte-identical with and without it for [3,4], [4,5] and [3,5], and exactly double for [3,3] and [4,4].

---

The problem

For colour targets t_1..t_r and a budget of j wildcards,

w(j+r; 2^j, t_1..t_r) = 1 + max{ n : [1,n] can be split into j singleton
                                 classes and r colour classes, where colour
                                 class i contains no t_i-term arithmetic
                                 progression }

The 2^j is j colours whose target is 2 — a class with target 2 can hold at most one element, which is why they behave as wildcards.

A217058(j) = w(j+2; 2^j, 3, 4): one colour must avoid 3-term APs, the other must avoid 4-term APs. Published terms, offset 0:

a(0..11) = 18, 21, 25, 29, 33, 36, 40, 42, 45, 48, 52, 55

Establishing the next term a(12) needs two independent halves:

half	claim	how it is checked
lower bound	a valid colouring of [1, a(12)−1] exists	a certificate — check it yourself, no solver involved
upper bound	no valid colouring of [1, a(12)] exists	a SAT refutation — this is the half that needs auditing

Verifying a lower bound yourself

The certificate is a string over {., 1, 2}: . is a wildcard, 1 and 2 are the two real colours. verify_certificate.py depends on nothing but the standard library and never touches a SAT solver — it just reads the string and applies the definition.

python vdw/verify_certificate.py "$(cat vdw/cert_n56.txt)" 12 3 4
python vdw/verify_certificate.py --selftest     # controls, incl. negative ones

Why the upper bound is believable

"No colouring exists" asserts an absence, so it is only as good as the claim that the CNF handed to the solver really is the problem. Five independent guards:

1. encoding_audit.py — the CNF is exactly the definition. On instances small enough to enumerate exhaustively, the set of colourings satisfying the CNF is compared with the set a direct transcription of the definition accepts. Equal both ways on all 11 cases across 6 target shapes — one for every family claimed here: nothing invented, nothing lost.
2. Symmetry breaking never loses an orbit. The same audit checks that every orbit of the symmetry group (generated by the reversal i ↦ n+1−i and by swaps of equal-target colours) keeps at least one representative. Losing one is exactly how a satisfiable instance gets reported UNSAT. Zero lost.
3. vdw_validate.py — the engine reproduces what is already known. For a published a(j) = w, it must find a verified witness at w−1 and refute w. 29/29 published values across five families.
4. cross_check.py — a second, disjoint derivation. The answer is re-established with the older engine that has no reversal-symmetry constraint, a different CDCL solver, and a different cube depth.
5. scale_test.py — the wildcard budget at exact scale. The exhaustive audit reaches only small instances, so the totalizer is tested directly at n = 55..58, j = 12, from both sides: 240 at-limit assignments accepted, 240 over-limit rejected, and forcing 13 wildcards inside the full formula is correctly UNSAT.

Plus a structural rule in the runner: UNSAT is reported only when every cube has returned an explicit verdict. A worker killed by the OS raises; it is never silently read as "no solutions in this branch". Three earlier runs died to exactly that class of failure.

Layout

vdw/vdw4.py               engine: encoding, reversal symmetry, cube-and-conquer
vdw/vdw_probe.py          decide one instance, durably, with its own log
vdw/vdw_sat.py            randomised-restart portfolio for the satisfiable half
vdw/vdw_run.py            resumable driver + crash-honest parallel solve
vdw/encoding_audit.py     proves the CNF equals the definition, by exhaustion
vdw/vdw_validate.py       replays published values through the engine
vdw/verify_certificate.py standalone checker, stdlib only, trusts nothing
vdw/cross_check.py        independent re-derivation through a disjoint path
vdw/vdw2.py               earlier engine, kept as the cross-check's second opinion
maxvol/                   closed thread, kept for the record; nothing below
                          depends on it

Reproducing

Needs Python 3.13, which is what CI runs, and one third-party package. There is nothing to build and nothing to install from this repository: it is a set of scripts and evidence files, not a package.

pip install python-sat==1.9.dev7
python verify_all.py

That second line is the whole thing. It re-checks every claim in this repository against the evidence committed beside it and prints EVERY CLAIM IN THIS REPOSITORY IS SUPPORTED BY EVIDENCE ON DISK only if all of them hold; anything else means do not believe the numbers below. On this machine it is 108 passed, 0 failed, 15 skipped; python verify_all.py --fast drops the two re-executed audits for 106 passed, 12 skipped. .github/workflows/ci.yml runs the full one on every push, after python scrub_paths.py --check.

The version is pinned because the audits re-derive results through that solver, and a gate whose verdict depends on the day it runs is not a gate. CaDiCaL ships inside python-sat, so no solver has to be installed separately. Note that pysat's Kissat404 hard-crashes the interpreter on this platform — a native abort with no Python exception — so it is excluded.

Two of the gate's sections skip rather than fail when what they need is absent, and say so in their own heading, with the skipped count folded into the final tally line (N passed, 0 failed, K skipped) rather than only appearing inside a section nobody has to read. The DRAT refutation replays want the kissat and drat-trim binaries, found on PATH, through KISSAT / DRAT_TRIM, or by flag — vdw/DRAT.md builds both without administrator rights and explains the Windows text-mode trap that silently truncates a proof. Neither ships as an apt or cargo package; CI should build both from source per vdw/DRAT.md (on Linux that is just cc -O2 -o drat-trim drat-trim.c for drat-trim and kissat's own ./configure && make) so this section actually runs instead of skipping on every push. The staging-folder sections want a local OEIS-upload directory, which is a one-person workbench, deliberately never committed, and absent on a CI runner by design. Everything else runs from a bare clone, including cube_certify.py's own verdict logic (vdw cube_certify --selftest, standalone below): kissat/drat-trim being absent used to mean cube_certify.py was imported by nothing in this gate at all, so a broken verdict there was as invisible as a broken verdict in code that had been deleted. The selftest calls certify_cube and parse_cube directly with the two external tools stood in for (their real DRAT proof-checking is exactly the thing the paragraph above is about) and checks that a genuine proof is ACCEPTED and one corrupted by the file's own --negctl-truncate control is REJECTED.

The individual pieces, if you want them one at a time rather than through the gate:

python vdw/encoding_audit.py                     # ~2 min
python vdw/vdw_validate.py quick Cadical195      # published values, cheap ones
python vdw/vdw_probe.py 58 12 3 4 --workers 8    # the upper bound, ~50 min

Worker count is deliberately capped well below the logical core count: each CaDiCaL grows an unbounded learned-clause database, and oversubscribing this machine exhausted RAM and orphaned worker processes that outlived their parent by hours.

Results

Five new terms, in five different families, all published lists standing since 2012:

sequence	new term	value	published before
A217058	a(12) = w(14; 2^12, 3, 4)	57	12 terms
A217005	a(19) = w(21; 2^19, 3, 3)	52	19 terms
A217007	a(7) = w(9; 2^7, 4, 4)	68	7 terms
A217059	a(9) = w(11; 2^9, 3, 5)	74	9 terms
A217236	a(4) = w(6; 2^4, 4, 5)	84	4 terms

A217058:  18, 21, 25, 29, 33, 36, 40, 42, 45, 48, 52, 55, 57
A217005:  9, 14, 17, 20, 21, 24, 25, 28, 31, 33, 35, 37, 39, 42, 44, 46, 48, 50, 51, 52
A217007:  35, 40, 53, 54, 56, 66, 67, 68
A217059:  22, 32, 43, 44, 50, 55, 61, 65, 70, 74
A217236:  55, 71, 75, 79, 84

Novelty for all five was confirmed against the live OEIS API, not against a paper.

A217058(12) = 57

Lower bound. This colouring of [1,56] uses exactly 12 wildcards, has no 3-term AP in colour 1 and no 4-term AP in colour 2, so a(12) > 56:

2.21221212.12.22211.112.2221.222.2.1..12221211212..22212

Check it yourself in milliseconds, trusting none of this code:

python vdw/verify_certificate.py "2.21221212.12.22211.112.2221.222.2.1..12221211212..22212" 12 3 4

Upper bound. n=57 with j=12 is unsatisfiable, established three times over in three symmetry configurations:

encoding	solver	cubes	verdict	time
vdw4, reversal symmetry on	CaDiCaL 1.9.5	k=4	UNSAT	6257 s
vdw2, no symmetry breaking at all	CaDiCaL 1.9.5	k=4	UNSAT	8037 s
vdw4, reversal symmetry off	CaDiCaL 1.9.5	k=4	UNSAT	8317 s

The middle row is the one that matters: it searches the full unreduced space, so it cannot inherit an error from the lex-leader constraint that is the only new mathematics in the engine. Separately, a randomised-restart portfolio spent 8 rounds × 5 seeds × 3M conflicts hunting a witness at n=57 and found none.

These runs do not check the encoding. All three build the formula the same way — same AP enumeration, same exactly-one blocks, same totalizer call, same CaDiCaL through pysat — so an error there would survive all three. They differ only in which symmetry-breaking constraints are active, which is what they test. The encoding is checked separately against the definition (vdw/encoding_audit.py).

The step from a(11) = 55 is +2. That is not anomalous — +2 already occurs in the published sequence at a(6) = 40 → a(7) = 42.

A217005(19) = 52

Both colour classes must avoid 3-term APs. Lower bound — this colouring of [1,51] uses exactly 19 wildcards with no 3-term AP in either class:

..11.1122.2211.1122.22.........11.1122.2211.1122.22

Upper bound — n=52, j=19 is unsatisfiable, all 36 cubes reporting.

This family exercises a code path the first result never touched: its targets are equal, so the colour-swap symmetry breaker is active, whereas on [3,4] it emits no clauses at all. Its full-scale gate passed first — published a(18)=51 reproduced exactly, SAT at n=50 and UNSAT at n=51.

A217007(7) = 68

Both colour classes must avoid 4-term APs — the first family here where the targets are 4 rather than 3, so the AP-enumeration is over a different and much larger set of progressions. Lower bound — this colouring of [1,67] uses exactly 7 wildcards with no 4-term AP in either class:

..1112112111.2221221222.1112112111.2221221222.1112112111.2221221222

Upper bound — n=68, j=7 is unsatisfiable, 7269 s, all 40 cubes reporting.

Its full-scale gate passed first: published a(6) = 67 reproduced exactly, SAT at n=66 with a verified witness and UNSAT at n=67.

An honest note on the lower bound. That certificate is the gate's own a(6) = 67 colouring with one extra wildcard prepended. Every new term hands the next one a free lower bound that way — a valid colouring of [1, a(j)−1] plus one more wildcard is a valid colouring of [1, a(j)] with j+1 wildcards — so a(7) ≥ 68 was known before any search ran. The solver was given the instance cold and rediscovered that construction rather than finding a richer one; it is recorded here as confirmation, not as independent evidence. All the weight sits on the upper bound.

The step from a(6) = 67 is +1, the smallest possible. That is not anomalous either: +1 already occurs twice in the published sequence, at a(2) = 53 → a(3) = 54 and at a(5) = 66 → a(6) = 67.

A217059(9) = 74

Colour 1 must avoid 3-term APs, colour 2 must avoid 5-term APs. Lower bound — this colouring of [1,73] uses exactly 9 wildcards:

21121222212222.22221122112..2.2222.2222.2122..2211221212222.2222121221122

Upper bound — n=74, j=9 is unsatisfiable, 3860 s, all 76 cubes reporting.

This lower bound was earned, not inherited. Unlike A217007, the certificate is not the free append-wildcard construction: the free bound from a(8) = 70 only gives a(9) >= 71, and it turned out to be three short. Explicit witnesses were found by search at n = 71, 72 and 73 in turn, each verified, each raising the floor. The n=73 witness came from cube 64 of 76 after 3464 s of searching — a genuinely independent object rather than a relabelled copy of the previous term's colouring.

How the value was cornered. Climbing one n at a time was costing 1000-3500 s per step and produced no ceiling at all, so the search was bracketed instead: a probe at n=75 refuted immediately-above, capping the answer at 75, while the climb pushed the floor to 74. That left exactly one undecided instance, n=74, and one run settled it. Satisfiability is monotone in n, which is what makes bracketing valid.

The step from a(8) = 70 is +4. The published differences are 10, 11, 1, 6, 5, 6, 4, 5, so +4 already occurs at a(6) = 61 -> a(7) = 65.

Cross-checked, like the others. The refutation at n=74 was re-derived twice more in other symmetry configurations: vdw2, which carries no symmetry-breaking constraint at all, returned UNSAT in 3453 s, and the primary engine with reversal symmetry disabled returned UNSAT in 3460 s. vdw2 also found and verified a witness of its own at n=73 (2416 s). Recorded in vdw/crosscheck_a9.json, AGREES. All five terms were refuted in three symmetry configurations.

A217236(4) = 84

Colour 1 must avoid 4-term APs, colour 2 must avoid 5-term APs — the largest pair of targets of the five families, over the shortest published list: four terms. Lower bound — this colouring of [1,83] uses exactly 4 wildcards:

122121221221212221.212121221121222211121.221212222.2222.212211211122221211122212122

python vdw/verify_certificate.py "$(cat vdw/cert_A217236_a4_n83.txt)" 4 4 5

Upper bound — n=84, j=4 is unsatisfiable, 7965 s, all 80 cubes reporting.

Its full-scale gate passed first: published a(3) = 79 reproduced exactly, SAT at n=78 with a verified witness and UNSAT at n=79.

This lower bound was earned, not inherited. The free append-wildcard construction from a(3) = 79 only gives a(4) >= 80, four short of the truth. The witness at n=83 came from cube 52 of 80 after 6470 s of searching and was verified — an independent object rather than a relabelled copy of the previous term's colouring.

How the value was cornered. Bracketed rather than climbed: a probe at n=87 returned UNSAT and capped the answer, n=83 SAT lifted the floor, n=85 UNSAT tightened the cap, and one run at n=84 closed the remaining gap. Satisfiability is monotone in n, which is what makes bracketing valid.

Cross-checked, like the others. The refutation at n=84 was re-derived twice more in other symmetry configurations: vdw2, which carries no symmetry-breaking constraint at all, returned UNSAT in 10959 s, and the primary engine with reversal symmetry disabled returned UNSAT in 16975 s. vdw2 also found and verified a witness of its own at n=83 (9893 s). Recorded in vdw/crosscheck_a4.json, AGREES.

The step from a(3) = 79 is +5. The published differences are 16, 4, 4, so +5 is a first for this family; with only four published terms there is no strong prior either way.

Evidence summary

check	result
CNF ≡ definition, by exhaustive enumeration	11/11 cases, both directions
symmetry breaking loses an orbit	never — 0, anywhere
wildcard budget at n = 55…58, j = 12	240 at-limit kept, 240 over-limit rejected
published values replayed through the engine	29/29 across 5 families
full-scale gate: a(11) = 55 reproduced at j = 11	both halves
full-scale gate: a(3) = 79 reproduced at j = 3	both halves
every new term's refutation re-derived along two disjoint paths	5/5 AGREE
certificate under the standalone verifier	ACCEPTED

Each SUBMISSION_*.md is generated mechanically from the result files — the number cannot drift from what was computed, and the generator re-runs the verifier before writing. All five are now approved and live in the OEIS: A217058(12) on 30 July 2026, A217005(19), A217007(7) and A217236(4) on 7 August, and A217059(9) on 13 August, each credited in the entry's extensions line.

The entries themselves are the live state; this paragraph is checked against them rather than remembered, and the way to check it is to search OEIS for the author name rather than to list the sequence ids from memory.