How far can you get on R(5,5) with proofs you can check by hand?

The best known bounds on the Ramsey number $R(5,5)$ rest on decades of computer search, most recently about eighty processor-years of it. Primus asked a different question: how much of that result can be recovered by proofs a reader can verify from the page, with no computer in the loop? The answer is $38 \le R(5,5) \le 50$, and the paper shows exactly where, and why, the hand-checkable route runs out.

The problem

Take $n$ people at a party. Any two of them are either friends or strangers. The Ramsey number $R(s,t)$ is the smallest $n$ that guarantees either $s$ mutual friends or $t$ mutual strangers, no matter how the friendships fall. In graph language: every graph on $R(s,t)$ vertices contains a clique of size $s$ or an independent set of size $t$.

The small cases were settled by hand in 1955. $R(3,3) = 6$, $R(3,4) = 9$, $R(3,5) = 14$ and $R(4,4) = 18$. The next one up, $R(4,5) = 25$, needed a large computer search in 1995, since verified end to end in a proof assistant. And $R(5,5)$ is still open. The record is

$$43 \le R(5,5) \le 46,$$

where the lower bound comes from an explicit colouring on 42 vertices found by Exoo in 1989, and the upper bound comes from a 2024 computation by Angeltveit and McKay that consumed roughly eighty processor-years across two independent implementations. The experts' own view is that pushing further by the same route would need an unreasonable amount of computer time.

What "hand-checkable" means here

The paper sets itself a strict standard. Every definition is stated. Every step is justified by a named earlier step or a cited theorem. Every certificate, meaning every graph or subgraph that witnesses a bound, is displayed in closed form so a reader can check it with pencil and paper.

This is a trade-off, and the paper is explicit about which corner of it it occupies. A 2022 paper by Ge, Jayasooriya, Qiu, Sun and Yuan gave a fully hand-checkable proof that Exoo's 42-vertex colouring has no monochromatic $K_5$, so the record lower bound of 43 does have a proof on the page. It runs to about twenty pages of case analysis. Primus went the other way: accept a weaker bound in exchange for a certificate that fits on two pages, and buy the brevity with symmetry.

What the paper proves

• $R(5,5) \ge 38$, from the Paley graph on 37 vertices. A symmetry reduction brings the clique check down to a single eight-vertex subgraph, displayed as a table of quadratic residues, and the whole certificate fits on two pages.
• $R(5,5) \ge 37$ independently, via a self-contained proof of the Shearer–Mathon doubling construction, which the available literature only sketches.
• $R(5,5) \le 50$ from the classical recursion and the formally verified value $R(4,5) = 25$, the paper's one computational input. With no computational input at all, $R(5,5) \le 62$.
• Why the hand route stops there. The subgraph-counting identity that first pushed the upper bound to 49 turns out to be exactly feasible on 49 vertices, and the paper proves it cannot give a contradiction from extremal edge counts alone.

How this paper was made

This paper was produced by Primus in proof mode. Primus scoped the problem, reviewed the literature, wrote the research plan, developed the proofs, audited them, and wrote the paper. The displayed tables of quadratic residues and differences can also be confirmed by direct symbolic computation, and scripts that do so are among the project's artifacts.

• Browse the Primus research report →

The paper, with every proof written out in full, can be downloaded below.