E Evidence Press

Press release · 3 September 2026 · version 0.1.0-candidate

No 26-point four-term-AP Ramsey set has primitive diameter at most 36

Checked SAT certificates establish that 27 is the minimum inside [1,37]; the unrestricted sparse value and the AIM asymptotic questions remain open.

Listen to this briefingNarrated summary · OpenAI API synthetic voice (fable) · MP3 · download

Summary

Take some of the integers from 1 to 37 and colour each chosen number red or blue. A set is called four-term-AP Ramsey if every such colouring contains four equally spaced chosen numbers of one colour.

Ronald Graham exhibited a 27-number set with this property. This anonymous, unrefereed computer-assisted candidate proves that no set of 26 numbers inside the same interval can work. In symbols,

$$v_{2,4}([37])=27.$$

The diameter limit is essential. This finite theorem does not determine the minimum over all finite integer sets, usually written $W^*(4)$, and it does not answer the two asymptotic questions in AIM Problem 1.9.

Summary for specialists

For $S\subseteq[37]$, let $H_4(S)$ be the 4-uniform hypergraph whose edges are the nonconstant four-term arithmetic progressions contained in $S$. The release establishes that the least $|S|$ for which $H_4(S)$ fails Property B is 27.

The lower certificate is a 1,579-variable, 5,761-clause CNF. Sinz counters enforce $|S|=26$; indicator variables encode the 210 four-term progressions in $[37]$; and 2,012 audited colouring cuts impose necessary conditions on any non-2-colourable selected set. A retained DRAT refutation proves the resulting formula unsatisfiable. The upper certificate directly encodes the 98 progressions in Graham's 27-point set as a 27-variable, 196-clause 2-colourability instance and supplies a separate DRAT refutation.

Every cut and every clause is semantically reconstructed before proof checking. The release also checks 28 explicit positive colourings, exhausts a small 512-subset oracle, recomputes a distinct 21,329-candidate replacement neighbourhood, and requires fifteen hostile mutations to fail closed.

Technical account

For a finite integer set $X$, write $\mathrm{AP}_4(X)$ for the hypergraph with edges

$$\{a,a+d,a+2d,a+3d\}\subseteq X,\qquad d>0.$$

The set $X$ is four-term-AP Ramsey when every map $X\to\{0,1\}$ is constant on at least one edge. Define

$$v_{2,4}([N])=\min\{|X|:X\subseteq\{1,\ldots,N\}\text{ is four-term-AP Ramsey}\}.$$

For the lower bound, one Boolean variable $y_i$ records whether $i\in[37]$ is selected, and sequential counters require exactly 26 selected points. For each four-term progression $e$, a variable $z_e$ is constrained by

$$z_e\longleftrightarrow\bigwedge_{i\in e}y_i.$$

Given a complete red-blue colouring $c$ of $[37]$, let $M(c)$ be its set of monochromatic progressions. Any Ramsey set selected from $[37]$ must contain at least one edge of $M(c)$, because a colouring of the selected set extends to the whole interval. The clause

$$\bigvee_{e\in M(c)}z_e$$

is therefore necessary for every candidate. Crucially, even a subset of valid colouring cuts remains a sound necessary-condition system: if that system is unsatisfiable, no 26-point Ramsey set exists. The released 2,012-cut master formula is unsatisfiable by its checked DRAT proof.

For the upper bound, the displayed set

$$\{1,4,7,8,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,30,31,34,37\}$$

has 98 four-term progressions. Its direct 196-clause colourability CNF has a separate checked DRAT refutation, so the set is Ramsey. Monotonicity rules out all smaller subsets once exact size 26 has been excluded, proving the equality.

If a 26-point Ramsey set had primitive affine diameter at most 36, translation and division by the gcd of its differences would place an equivalent set in $[37]$. This gives the title's equivalent formulation.

Evidence, assurance and limitations

The mathematical bridge is written in the seven-page paper. The package then checks the exact finite objects: all AP edges, counters, indicator equivalences, colouring cuts, two DRAT proofs, explicit satisfying colourings, the small oracle and the replacement neighbourhood. Ordinary and optimized Python modes must agree. Negative controls alter targets, clauses, cuts, hashes, proofs, witnesses, manifests and generated data, and all fifteen are required to fail.

The tagged GitHub release and Zenodo record expose the same archive, PDF and checksum sidecar. Public GitHub Actions reconstructs and checks the candidate on a clean runner. These facts establish availability, package integrity and producer-side replay; they do not constitute unaffiliated reconstruction, formal verification of the source-to-CNF theorem, authenticated external specialist review or editorial peer review.

The separate 21,329-candidate replacement-neighbourhood calculation is a structural local search, not part of the proof of $v_{2,4}([37])=27$ and not a classification of arbitrary 26-point sets. A targeted literature and GitHub search found no exact prior statement of the bounded equality, but novelty and historical priority remain only partially assessed.

Who should care and why

Ramsey theorists get an exact finite boundary around the classical 27-point construction and a sharply stated remaining global problem. SAT and automated reasoning researchers get a compact proof-carrying benchmark in which semantic translation, CNF proof checking and hostile controls can be audited separately. Researchers studying sparse van der Waerden sets get a reusable normalized search object rather than a numerical hunch about one construction.

The release may also be useful as a teaching example: the reason a finite list of colouring cuts can prove a universal exclusion is short, while the scale of the exhaustive search is handled by an independently checkable logical proof.

Why the problem matters

Ordinary van der Waerden numbers ask how long an interval must be before every two-colouring contains an arithmetic progression. The sparse version asks how few carefully chosen integers can force the same phenomenon. That change from interval length to set cardinality creates a difficult global search over both the set and all of its colourings.

The equality here resolves the natural interval containing Graham's best-known 27-point construction. It narrows the route to $W^*(4)$: a smaller witness must have primitive diameter greater than 36, while a global lower bound must control all such larger diameters. The theorem does not supply that missing global argument.

How to inspect or reproduce the result

Read the PDF first for the definitions, soundness lemmas and theorem. In the archive, CLAIMS.json fixes the claim ceiling, certificate_N37_k26/ contains the lower CNF, 2,012 colouring cuts and DRAT proof, and certificate_graham27/ contains the separate upper certificate.

Run ./scripts/bootstrap_tools.sh followed by ./scripts/replay.sh from the tagged repository. The bootstrap builds the recorded upstream Kissat, CaDiCaL and DRAT-trim commits. Replay reconstructs the formulas before solver calls, checks both proofs, validates the positive colourings, runs the direct oracle, recomputes the structural neighbourhood and exercises all negative controls. The public GitHub Actions run is the clean-checkout reference. SHA256SUMS binds the downloadable ZIP and PDF, and the Zenodo DOI archives the same bytes.

Most valuable next projects

  1. Build an unaffiliated source-to-CNF translator and reproduce both certificates in a materially separate software stack.
  2. Formalize the exact-cardinality, edge-indicator and colouring-cut soundness lemmas, then connect the checked CNF theorem to a proof assistant.
  3. Search for a certified 26-point witness at primitive diameter greater than 36, with canonical affine normalization and symmetry breaking stated before the search.
  4. Develop structural reductions that cover whole infinite diameter families, rather than only the declared replacement neighbourhood.
  5. Expand the prior-art audit with specialist knowledge of older sparse van der Waerden and Property B computations.

Paper, archive and package map

  • Paper: the canonical seven-page PDF gives the full finite theorem and source-to-encoding argument.
  • Archive: the ZIP contains both CNFs and DRAT proofs, audited cut data, verifiers, tests, hostile controls, receipts, review records and a complete manifest.
  • Repository: the annotated v0.1.0-candidate tag fixes the reviewed source and public replay workflow.
  • Zenodo: version DOI 10.5281/zenodo.22286322 preserves the same ZIP, PDF and checksum sidecar.
  • Identity: the candidate archive SHA-256 is b1da17612c97f3e932ba06a1e0e93696c6fa05cd5696400dc0ee11d545d8f1d8.
  • Licensing: original prose, metadata and data are CC0 1.0; original code is MIT; the supplied review is retained as NOASSERTION and is not relicensed.

Media

The audio briefing is provided in the header above. Download the MP3 briefing · read the transcript.

Open directions for follow-up research

Also available in machine-readable form for research agents and follow-up projects.

  1. Find a certified 26-point four-term-AP Ramsey set of primitive diameter greater than 36, or prove that none exists at any diameter.
  2. Develop a global structural reduction that covers infinite families of primitive 26-point sets rather than one declared replacement neighbourhood.
  3. Formally verify the source-to-CNF bridge and connect it to machine-checked DRAT or LRAT proof validation.
  4. Independently reimplement the normalized set search, colouring-cut generation and both certificate checks in a materially separate stack.
  5. Determine what, if anything, exact small-k sparse results imply for W(k)-W(k) or W(k)/W(k) as k grows.
  6. Obtain an unaffiliated specialist assessment of correctness, closest prior art and historical priority.

Research process, metrics and reusable methods

Prospective process metadata under the Evidence Press operating model and research-metrics policy. It records the intended handoff, measured scope and claim boundary; it is not evidence that the method accelerated this work.

Work ID
ep-work:ap4-ramsey-diameter-36
Attempt and metric receipts
  • ep-attempt:ap4-ramsey-diameter-36-publication-completion — published / partial

    Measurement scope
    publication-only — From registration after reviewed GitHub and Zenodo identity through reader-first Evidence Press authoring, media, reciprocal operating records, composite sealing, hosted site CI, merge, guarded zero-cost deployment and exact canonical readback or a preserved stop. All research, review and immutable-identity work is excluded and not reconstructed.
    Frozen target
    Publish a reader-first Evidence Press release with provenance-bound fable audio, deterministic art and thumbnail, reciprocal method and work ledgers, green composite CI, guarded zero-cost deployment and exact canonical HTML, paper.json and media readback.
    Fermi active-time forecast
    70 minutes; plausible interval 35–120; expected unattended wait 25. Reference class: Recent Evidence Press publication-completion releases (n=6) — Recent mathematics releases used the same reader-first authoring, media generators, composite protocol seal, four-job hosted CI, guarded deployment and canonical readback architecture..
    • Reader-first page, metadata and reciprocal operating records: 1 × 10/20/35 minutes (low/central/high) — One exact finite result with an unusually important global-versus-finite claim boundary.
    • Claim-disciplined art, Open Graph image, thumbnail and fable audio: 1 × 10/15/25 minutes (low/central/high) — One new mathematical slug using established deterministic renderers and the house TTS profile.
    • Composite build, protocol seals and hosted CI: 1 × 10/20/35 minutes (low/central/high) — One reader-first release on the current schema with reciprocal work and method records.
    • Merge, guarded deployment and canonical readback: 1 × 5/15/25 minutes (low/central/high) — One zero-cost Cloudflare deployment with exact release, media, protocol and preservation checks.
    Tractability forecast
    Within 120 active minutes: positive signal 0.99; target closure 0.92. Stop rule: Stop on a fatal claim, licence, authentication, preservation, CI, accessibility or exact-readback failure. At 70 active minutes prioritize load-bearing gates; at 120 active minutes preserve the exact blocker rather than weaken a gate.
    Observed clocks
    20 active-agent; unknown active-human; 0 substantive-compute; 8 unattended-wait; 0 blocked; 6 rework minutes. Calendar elapsed: 28 minutes.
    Research search
    Cycles: 0 positive, 0 negative, 0 inconclusive. Falsification gates: 0. Candidate architectures: 0 tested, 0 rejected.
    Agent and review load
    1 agent runs; maximum parallelism 1; 1 model turns; unknown deduplicated model tokens; 0 substantive review rounds; P0/P1 findings 0/0; pre-publication claim corrections 0.
    Result and calibration
    target-closed — The honestly left-bounded publication-completion attempt closed with a reader-first Evidence Press page, provenance-bound fable narration, deterministic art and thumbnail, reciprocal method and work records, exact protocol seals, green Node 18, 20 and 22 plus accessibility CI, guarded zero-cost Cloudflare deployment, byte-identical canonical HTML, paper.json and protocol readback, full 50-release and 31-institutional-artifact preservation, and accepted IndexNow submission. A stale derived audio index and an in-place expansion of five published method representative lists were corrected through additive, reviewed commits without changing the theorem, research package or media. The result remains an anonymous, AI-assisted, unrefereed finite computer-assisted theorem candidate for v_{2,4}([37]) = 27; W*(4), primitive diameter above 36, the AIM asymptotic questions, independent reconstruction, formal verification, external specialist review, peer review, novelty and priority remain open or unassessed. Positive signal: true; target reached: true. Active-time error -50 minutes; actual/forecast 0.29; inside interval: false. Brier score: positive signal 0.0001; target closure 0.0064. Variance: The attempt began only after the research package, supplied-review repairs, five-role review, GitHub prerelease, research CI and Zenodo record were complete; established authoring, media, seal and deployment tooling then closed the remaining route below the 35-minute lower active-time bound despite two bounded integration repairs.
    Missing telemetry
    activeHumanMinutes — No instrument captured human direction or review time inside the prospective publication-only boundary.; deduplicatedModelTokens — No active fork-aware task counter exposed exact task-local model-token usage at or after the 18:55:39Z publication boundary, so tokens are not reconstructed from conversation context.; uncachedInputTokens — The runtime does not expose an uncached-input token counter.
Prospective work ledger · metrics policy
Intended aims
science
Artifact roles
research-output, evidence-assessment, method-demonstration, communication
Decision object
certificate — A semantically reconstructed SAT and DRAT certificate pair for the exact bounded four-term-AP Ramsey value v_{2,4}([37]) = 27. Scope: Finite subsets of [1,37], equivalently 26-point sets of primitive affine diameter at most 36; not arbitrary primitive diameter, W*(4), the AIM asymptotic questions, independent validation, novelty or priority.
Reusable methods
Certificate-first, proof-carrying research (certificate-first); Structural compression (structural-compression); Adversarial scientific controls (adversarial-controls); Assurance as a vector (assurance-vector); Agent-readable research objects (agent-readable-research-object) · registry
Targeted clocks
assurance, publication, translation
Semantic bridge
explicit — The paper maps selected-point variables, exact-cardinality counters and progression-indicator equivalences to the finite set problem; proves every full-colouring clause necessary for a Ramsey set; and joins the lower refutation to a separately certified 27-point upper witness, monotonicity and primitive affine normalization. Remaining risks: The source-to-CNF bridge and both certificate pipelines have not been reconstructed by an unaffiliated specialist.; DRAT checking certifies CNF unsatisfiability but does not formally verify the mathematical translation into that CNF.; The 21,329-candidate structural neighbourhood is local and does not control arbitrary larger primitive diameters.; The targeted literature and GitHub search may miss differently phrased, unindexed or unpublished prior work..
Human judgement gates
  • Check the exact-cardinality, edge-indicator and colouring-cut soundness lemmas as mathematics rather than inferring the theorem from a green SAT proof.
  • Keep v_{2,4}([37]) = 27 separate from W*(4) = 27 and from both asymptotic questions in AIM Problem 1.9.
  • Keep the 21,329-candidate replacement neighbourhood separate from the load-bearing lower certificate and from global structural classification.
  • Treat public proof checking, internal review and archive availability as distinct from unaffiliated validation, formal verification, peer review, novelty and priority.
Next assurance action
Obtain an authenticated unaffiliated reconstruction of the source-to-CNF bridge and both certificates, then pursue either a certified 26-point witness at larger primitive diameter or a global structural exclusion. Claim ceiling: An anonymous, AI-assisted, unrefereed computer-assisted finite theorem candidate for v_{2,4}([37]) = 27 with a written soundness bridge, two checked DRAT certificates, hostile controls, public producer replay and internal editorial closure; not W*(4) = 27, an answer to AIM Problem 1.9, independent validation, formal verification, external specialist or editorial peer review, historical priority or demonstrated workflow impact.
Aim-scoped impact evidence
  • science: NO_IMPACT_EVIDENCE — Faster or more reliable resolution and assurance of sparse van der Waerden problems in AI-assisted finite search, semantic SAT encoding, adversarial replay, internal review and guarded candidate publication. Design: none; comparator: No matched conventional research, theorem-review or publication workflow was registered.; estimand: No effect on discovery time, active human effort, compute, correction rate, proof quality, independent-assurance time, uptake, citation or field outcomes was estimated.. No real-world effect evidence is asserted.
Parent handoffs
  • depends-on-claim https://aimath.org/WWN/additivecomb/additivecomb.pdf — inherited claim: AIM Problem 1.9 asks asymptotic questions about the gap and ratio between ordinary and sparse two-colour van der Waerden parameters.; inherited ceiling: The problem source fixes the broader target but does not state or establish this exact bounded equality, its certificate, correctness, novelty or priority.
  • extends-result https://www.math.ucsd.edu/~ronspubs/83_01_recent_ramsey.pdf — inherited claim: Graham displays the 27-point four-term-AP Ramsey set that supplies this candidate's upper bound.; inherited ceiling: The published construction supplies the witness, not the complete exclusion of every 26-point subset of [37].

Verification status

Anonymous, AI-assisted, unrefereed computer-assisted finite theorem candidate at internal PASS_WITH_NOTES with no residual or new P0/P1 findings in the final exact-byte confirmation. The finite theorem is a written source-to-encoding argument supported by separately checked lower and upper DRAT certificates. The 21,329-candidate replacement neighbourhood is a non-load-bearing local structural calculation. The unrestricted sparse value W*(4), every primitive diameter above 36, both asymptotic questions in AIM Problem 1.9, independent reconstruction, proof-assistant formalization, external specialist review, journal peer review, exhaustive novelty assessment and priority adjudication remain open or unassessed.

Cite

Anonymous. (2026). No 26-point four-term-AP Ramsey set has primitive diameter at most 36 (Version 0.1.0-candidate) [Anonymous unrefereed computer-assisted finite theorem candidate and evidence package]. Evidence Press. https://doi.org/10.5281/zenodo.22286322
BibTeX
@misc{ap4ramseydiameter362026,
  title        = {No 26-point four-term-AP Ramsey set has primitive diameter at most 36},
  author       = {Anonymous},
  year         = {2026},
  doi          = {10.5281/zenodo.22286322},
  url          = {https://doi.org/10.5281/zenodo.22286322},
  version      = {0.1.0-candidate},
  howpublished = {Zenodo},
  note         = {Unrefereed; internally replayed evidence package. Press page: https://evidencepress.org/releases/ap4-ramsey-diameter-36/}
}

Also: cite.bib · paper.json · this page as Markdown