cert-machine · audit · AlphaEvolve's Ramsey graphs · found 2026-10-23 at google-research 0d94f8c4

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

Each graph decided by an exhaustive search, in two implementations held to each other

With AlphaEvolve (arXiv 2603.09172) Google released 18 graphs, one per claimed lower bound on a Ramsey number R(s, t). A graph on m − 1 vertices with no clique of size s and no independent set of size t proves R(s, t) ≥ m. Here each file is read as a simple graph and both properties are decided by an exhaustive search written from the definition, in two implementations held to each other root by root: 16 of 18 CERTIFIED, 2 still searching.

Published, not peer-reviewed. The graphs and the bounds are Google's (Apache-2.0), copied unmodified from github.com/google-research/google-research at 0d94f8c4 and pinned by sha256; their sha256 equal those maximusrufus published with the same files (cert-machine#1). Neither Google's notebook nor maximusrufus's checker was run or read for this decision. A CERTIFIED file proves its bound; whether the bound is new is the paper's claim, not checked here.

tl;dr
  • The finding. 16 of 18 files prove their bounds; none fails. All 18 are simple graphs of the order their names claim. The 13 graphs up to 250 vertices were searched to the end on both sides by both implementations, with equal node counts at every root. Of the 5 large graphs, every clique side is closed; the independent-set side of R(7, 13) >= 513, R(8, 18) >= 1052 is still being searched (57/512 roots, 0/1051 roots). Two gaps in the release's own check, neither of which changes a verdict, lead below.
  • The mechanism. For each side, every clique of the forbidden size would start at its lowest-ranked vertex in a smallest-last order and lie among that vertex's later neighbours; each such root is searched with a greedy colouring as the bound (c colour classes are independent sets, so no clique among them is larger than c). A branch closes only on that bound or on too few candidates — both theorems — so "none" means none. A "found" answer would print the vertices and be re-checked edge by edge without the search.
  • Check it. python3 tools/run-ramsey-ledger.py --check re-checks the pins, re-searches the small graphs with both implementations, re-reads every long search from its per-root record, fires a planted triangle and a planted independent set, refuses four malformed matrices and decides 24 random graphs both ways (seconds); python3 tools/run-ramsey-ledger.py --only R_8_12_ge_511 --fresh --budget 0 re-runs a long search from nothing (16 min on an 8-core M2).
files decided
16 CERTIFIED · 2 REFUSED
Google's 18 released graphs, google-research 0d94f8c4, ramsey_number_bounds/improved_bounds.
both implementations
13 of 13
Graphs up to 250 vertices: the C kernel and the Python reference count the same search nodes at every root, on both sides.
largest search closed
88,209,553,369 nodes
One side, every root to the end.
release's own check
unexecuted
verify_bounds.ipynb ships with 0 outputs and no execution count.
§1 · the gaps

What the release's own check leaves out

G1 · record · found 2026-10-23

The verifier ships unexecuted. The release's check is a notebook, verify_bounds.ipynb, which lists every clique of size s in the graph and every clique of size t in its complement with igraph's cliques(min=k, max=k). It is published with 0 output cells and no execution count, so the release carries no record that the check was run on any file, or how long the five large ones took.

What would close it. The notebook's output, or the run's log and timing, beside the files.

G2 · reading · found 2026-10-23

Half the matrix is read. The notebook builds the graph from the entries above the diagonal that equal 1. Symmetry and the diagonal are never looked at, and an entry other than 0 or 1 would be read as "no edge". All 18 files are in fact symmetric 0/1 matrices with a zero diagonal (checked here, instruments/ramsey/graph.py), so no verdict changes; a file that was not would have been "verified" as the graph of its upper triangle.

What would close it. Three assertions before the graph is built: square, symmetric, zero diagonal, entries in {0, 1}.

§2 · the decisions

Every file, both sides

claimverticesno s-clique (K side)no independent t-set (I side)both implementationsverdict
R(3, 12) >= 5352none · 52 nodesnone · 4,967 nodesyes, root by rootCERTIFIED
R(3, 13) >= 6160none · 60 nodesnone · 54,515 nodesyes, root by rootCERTIFIED
R(3, 15) >= 7473none · 73 nodesnone · 130,758 nodesyes, root by rootCERTIFIED
R(3, 17) >= 9392none · 92 nodesnone · 1,730,104 nodesyes, root by rootCERTIFIED
R(3, 18) >= 10099none · 99 nodesnone · 1,423,686 nodesyes, root by rootCERTIFIED
R(4, 13) >= 139138none · 1,371 nodesnone · 250,304 nodesyes, root by rootCERTIFIED
R(4, 14) >= 148147none · 1,300 nodesnone · 1,038,704 nodesyes, root by rootCERTIFIED
R(4, 15) >= 163162none · 1,716 nodesnone · 2,344,398 nodesyes, root by rootCERTIFIED
R(4, 16) >= 174173none · 1,689 nodesnone · 5,024,559 nodesyes, root by rootCERTIFIED
R(4, 18) >= 209208none · 2,793 nodesnone · 10,754,608 nodesyes, root by rootCERTIFIED
R(4, 19) >= 219218none · 2,722 nodesnone · 16,226,653 nodesyes, root by rootCERTIFIED
R(4, 20) >= 237236none · 3,612 nodesnone · 10,401,596 nodesyes, root by rootCERTIFIED
R(4, 21) >= 244243none · 3,488 nodesnone · 17,515,703 nodesyes, root by rootCERTIFIED
R(8, 12) >= 511510none · 1,805,950 nodesnone · 23,489,926,261 nodeskernel; roots on recordCERTIFIED
R(7, 13) >= 513512none · 2,399,667 nodes57 / 512 roots · 46,390,841,578 nodeskernel; roots on recordREFUSED
R(9, 11) >= 617616none · 79,590,364 nodesnone · 10,998,244,950 nodeskernel; roots on recordCERTIFIED
R(10, 12) >= 856855none · 503,223,948 nodesnone · 88,209,553,369 nodeskernel; roots on recordCERTIFIED
R(8, 18) >= 10521051none · 18,979,448 nodes0 / 1051 roots · 0 nodeskernel; roots on recordREFUSED

Node counts are search nodes of this algorithm, comparable between its two implementations and across runs, not across programs. A long side's finished roots are kept in corpus/ramsey/runs/<file>.<side>.progress ("rank nodes"), so a stopped search resumes and every closed root stays on record.

§3 · the method

An exhaustive search, stated so it can be held to

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.

§4 · what is claimed, and what is not

The limits