Graham's $100 question: the twelve blocks are optimal

Let V(n) be the least number of monochromatic progressions {a, a+d, a+2d}, d ≥ 1, over all two-colourings of {1, …, n}. Graham proposed determining β in V(n) = βn²(1 + o(1)) as a $100 problem at the Erdős conference in Budapest in 1999. Parrilo, Robertson and Saracino (2008) disproved the folklore guess β = 1/16 with a colouring in twelve blocks of relative lengths

which gives 117/2192 ≈ 0.053376, and proved β ≥ 1675/32768 ≈ 0.051117 by a semidefinite relaxation. Butler, Costello and Graham (2010) recovered the twelve blocks by experiment, crediting the 2008 paper; Greenwood, Kariv and Williams (2023) proved them optimal among antisymmetric colourings with at most twelve blocks. On erdosproblems.com the question is problem #1186, for every k — open as of the snapshot pinned here (5 October 2026).

1 · Reduction. Counting each non-monochromatic progression by its two bichromatic pairs gives, uniformly over colourings, V(n)/n² ≥ 1/16 + Q*/4 − O(1/n), where Q* is the infimum over measurable φ : [0,1] → [−1,1] of

The twelve-block function φ* has Q(φ*) = -5/137, and 1/16 − 5/548 = 117/2192; so everything rests on Q ≥ −5/137. 2 · Expansion. Write φ = φ*(1 − 2σ) with σ ∈ [0, 1] the part flipped against φ*. Exactly, for every φ,

and h is piecewise linear on the 1/1096 grid, zero exactly at the eleven edges, with ∫h = 5/137. 3 · Discretisation without first-order loss. On cells whose ends include every edge, the bathtub principle bounds ∫hσ cell by cell with no loss at σ = 0, and pairs of cells cut by the boundary of R are bounded from 0 ≤ σ ≤ 1 alone; the resulting quadratic L(y) in the cell averages satisfies E ≥ L. 4 · Cover. By the symmetry φ → −φ it suffices to take m = ∫σ ≤ ½; five regions in m each carry an exact certificate that L is ≥ 0 (the region nearest the optimum) or strictly positive (the other four).

Step 3 is the whole idea. Discretising φ itself, as every relaxation since 2008 did, gives away a first-order amount at every cell pair the boundary of R crosses — and that loss caps the bound below the answer however fine the grid (§5). In σ the first-order term is ∫hσ, which the bathtub bounds exactly; what is lost is second order.

The claimant's check. The generators and a verifier were written in the sandbox in one session, by one AI agent, separately from each other. That verifier, kept here as an exhibit and re-run from the pinned bytes, accepts the five files (87 s on this machine). It leaves the gap the claimant named itself: a misreading shared by generator and verifier would not be caught.

The second verifier. instruments/delta3/verify.js was written afterwards, in JavaScript, by an agent given the mathematics and a field-by-field description of the files — not the generators, not the claimant's verifier, not its logs; the claimant's code entered this repository only after it was finished. It derives everything with proof force itself, in BigInt rationals: the colouring, h and its zeros, every cell area by two exact routes that must agree pair by pair (the trapezoid rule on the section length, and polygon clipping), the bathtub constants, the cut bounds, the residual matrices. It refuses any form it cannot show nonnegative and any multiplier of the wrong sign, and proves semidefiniteness exactly or refuses. It accepts all five in 0.8 s, and its exact bounds equal the files' claims.

Forgeries. node instruments/delta3/battery.js mutates genuine certificates and requires each mutation refused, by the rule it breaks: raised bounds (by 10⁻³ and by 10⁻⁶ — the certificates are that tight), dropped triangle forms, every θ set to 1 or to 0, widened slabs, ε set to 0 or inflated with B, a grid missing an edge of φ*, a doubled inner radius, an overspent linear budget, dropped inner multipliers, missing regions, and planted single entries off by 2⁻¹⁰⁰ — a negative multiplier, a sign-violating or repeated-index triangle, θ outside [0, 1], an unknown form. 40 of 40 refused at this build, 76 checks green. Then the verifier itself is mutated: 24 one-line edits (flip h, mirror R, drop ε, an optimistic cut bound, skip a sign check, trust the float Cholesky, accept a zero pivot …), 23 caught by the genuine set or a forgery; the one survivor removes a rule that is enforced twice.

The two lemmas, tested. The expansion identity and the discretisation lemma are proved on paper; they are also tested exactly on step functions finer than the grids, adversarial ones included: 1,400 cases of the identity, all equal; 4,200 cases of the lemma, all satisfied, the gap exactly 0 on breakpoint flips and single cells — the bound is sharp there. Tests, not proofs.

The upper bound, counted. The exact number of monochromatic progressions of the twelve-block colouring itself. For n a multiple of 1096 it is exactly 117n²/2192 − n/2:

A day earlier the same sandbox certified lower bounds the classical way — φ discretised on L equal cells, a Shor relaxation with triangle cuts, exact rational multipliers. Its verifier accepted δ₃ ≥ 0.05324921 at L = 256 (these were not re-decided here; the logs are kept as the claimant's). But the model's own minimum, found by local search, also stays below the answer at every L: every cell pair the boundary crosses gives away a first-order amount, so no grid refinement closes the gap. That measurement is what moved the proof into the coordinates σ.

• a referee The mathematics is two pages (the reduction, the expansion, the bathtub and discretisation lemmas). The author read it line by line on 5 October 2026, after both verifiers had accepted the certificates — the condition the erdosproblems forum sets before an AI-assisted solution is posted. No referee has read it.
• Lean Nothing is formalised. The finite part (five rational identities, semidefiniteness of 131- to 147-dimensional rational matrices) is plausible with a verified checker; the analytic part (the reduction, the bathtub rearrangement, the discretisation) is real measure-theory work — weeks, not days.
• independence Both verifiers and the generators were written by AI agents. The clean-room rule removes shared code, not a shared misreading of the mathematics both were given; §2 is where a reader should look.
• reproducibility of generation The multipliers came from a nondeterministic solver, so regeneration gives different files. The five files are the record, pinned by sha256; their force does not depend on regenerating them.