AlphaEvolve’s Ramsey lower bounds: the 18 released graphs decided

Reading. graph.py refuses a file that is not square, has an entry outside {0, 1}, is not symmetric, has a vertex joined to itself, or has a vertex count other than the m − 1 its name claims. The independent-set side searches the complement for cliques of size t.

Search. smallest-last (ties by smallest label); roots in rank order with their later neighbours; greedy colouring of the candidates (lowest label first), walked backwards; size + colour < k closes the branch. clique.py is the reference: standard library, agreeing with brute force on thousands of random small graphs. clique.c is the kernel, threaded over roots, held to the reference: the same order, the same colouring, the same branch order, so on every graph both finish the per-root node counts must be equal, or the build refuses.

Independence. Written from the definition of R(s, t). Google's notebook (igraph) and maximusrufus's checker were not run and their code was not read for this decision; the only things taken from the release are the 18 matrices and the claims in their file names.

• Claimed. For each CERTIFIED file: the pinned bytes are a simple graph on m − 1 vertices with no clique of size s and no independent set of size t, so R(s, t) ≥ m.
• Not claimed. That a bound is new or best known (the paper's comparison with the literature is not re-checked), anything about how AlphaEvolve found the graphs, or the code in the release's code/ directory.
• The trust in a "none". An exhaustive search has no short certificate. It rests on the algorithm (stated in full in clique.py), on its two implementations agreeing node for node where both run, and on the kernel for the large graphs alone.
• Independence. From Google and from maximusrufus, whose results on the same files (cert-machine#1) were read only after these were decided; not from the operator (one).

Decided 2026-10-27. Ramsey lower-bound graphs published by others than Google, decided by the same instruments; kept apart from Google's 18 and their counts. The contributor below had re-run two of our rows with their own code; this is the reciprocal check, kept apart from Google's counts.

• R(3, 33) >= 241 — CERTIFIED. JeetuSK0808 (Satyajeeth Suresh Kannan) (doi:10.5281/zenodo.23552014, pinned by sha256). The graph is rebuilt from the connection set the text prints (x ~ y iff y − x ∈ ±D on Z₂₄₀, 3,840 edges, equal to the certificate's edge list). No triangle (240 roots, 0.5 s). No independent set of size 33: the graph is circulant, so a translation moves any such set onto one through vertex 0, and the multipliers 1, 13, 37, 71, 169, 203, 227, 239 — each checked as an automorphism — fix 0 and split its non-neighbours into 31 orbits; orbital.c searched the 31 pieces this leaves (2,572 units, 2.9·10⁹ nodes, 537 s on 8 threads of the laptop) and found none. The reduction is a lemma proved in orbital.py's docstring and re-derived by it here; the kernel is held to it root by root on 78 smaller instances, with 8 red controls. The claimant's own proof needed orbital branching too, split into 1,665 jobs across three solvers. A second path that shares no code with the search — the same cubes as CNF formulas, solved by kissat with a DRAT proof, every UNSAT checked by drat-trim — closed 22 of the 31 cubes; the 9 largest stayed open at a 20-minute cap, so the second path is partial and the verdict rests on the orbital kernel (the summary is pinned beside the run in corpus/ramsey/runs).

• Re-run independently, 2026-10-24. maximusrufus (GitHub): Google’s AlphaEvolve Ramsey lower-bound graphs decided with their own clique search (two methods), before ours and with no code of ours: 15 of the 18 graphs, the verdicts compared with certs/ramsey-ledger.json. Outcome: the same verdict on all 15; R(10,12) and R(7,13), which they could not finish, decided here; R(8,18) unfinished on both sides. (their code · the report)
• Re-run independently, 2026-11-11. arhancanli (GitHub): R(3, 33) ≥ 241, JeetuSK0808’s circulant certificate, which we re-decided on 2026-10-27 (the outside row of certs/ramsey-ledger.json): replayed with their own code from the certificate data alone, none of the deposit’s programs read or run. The file’s graph is the Cayley graph of Z₂₄₀ on a symmetric set of 32 residues (3,840 edges), triangle-free by two routes, and it has no independent 33-set: the eight multipliers fixing 0 split its 207 non-neighbours into 31 orbits, and their own bitset branch and bound closed all 31 searches (19,242,156,924 nodes, 7,262 s of CPU on one core). Three red controls: with K = 32 the search finds an independent 32-set, with ±14 removed from the set it finds an independent 33-set, and on 60 random small circulants it agrees with brute force. Outcome: the same verdict: no triangle and no independent 33-set, through the same eight multipliers and the same 31 orbits. (their code · the report)
• Noted by an independent replayer, 2026-11-11. Arhancanli on GitHub, an independent replayer of the optimization-constants registry's certificates (quantavane-replays), with no connection to their authors: Replayed, with their own code and from the certificate data alone, the circulant certificate for R(3, 33) ≥ 241 that pull request #252 cites on the 17b page: triangle-free, and no independent 33-set in any of the 31 orbital searches, as our re-decision of 27 October on the same thread found. In their words: “It holds, in agreement with carlostoledo1891's re-decision above.” (the source, pinned)

Each credit is quoted from a snapshot pinned by sha256 (corpus/recognition.json); each re-run is a row of corpus/external-reruns.json. Neither is a peer review.