Featured publication · Liju James · 2026

Extension-rigidity of the known (5,5,42) Ramsey graphs

For every graph in the known catalogue, a machine-checked certificate shows that adding one vertex cannot produce a (5,5,43) graph.

Publication & artifacts ↗Research index

656Known graphs covered

328Representatives

CaDiCaL + kissatIndependent solvers

DRAT + Lean 4Proof evidence

The result

Each of the 328 representatives up to complementation from Brendan McKay's public catalogue produces a 42-variable extension CNF that is unsatisfiable. A machine-checked complement lemma transfers the result to all 656 known graphs.

A layered certificate

The artifact does not rely on one solver verdict. Each instance is processed by two independent SAT solvers; DRAT proofs are checked with drat-trim; each CNF is re-derived from its graph and compared clause for clause.

Controls against false confidence

Anti-vacuity checks on every unsatisfiable core
Delete-a-vertex positive controls that must return satisfiable, with witnesses checked
Two independent verification runs and recorded hashes
A Lean 4 exemplar certificate alongside the bulk proof pipeline

Exact boundary: the result proves extension-rigidity of the known catalogue. It does not prove that the catalogue is complete. Therefore R(5,5)=43 follows if and only if the McKay–Radziszowski completeness conjecture holds; the published unconditional bounds remain 43 ≤ R(5,5) ≤ 46.

Archive contents

The record supplies source graphs with provenance and hashes, all CNFs and DRAT proofs, verification tables from two runs, figures, standard-library Python code, and the compiled paper.