← All papers
An automated proof that R(B_8,B_10)=37
math.CO
Jun 4, 2026 · v1
TL;DR
Formalizes the upper-bound argument that every 37-vertex graph contains B_8 or B_10 in its complement, settling R(B_8,B_10)=37.
Abstract
We present a short proof that the book Ramsey number $R(B_8,B_{10})$ equals 37. The lower bound $R(B_8,B_{10}) \ge 37$ is already available in the literature, so it is enough to rule out a 37-vertex graph containing neither a copy of $B_8$ nor a copy of $B_{10}$ in its complement. The problem as well as the proof were found with AutoMath, an AI-assisted mathematical discovery workflow developed by the first author. A Lean formalization of the upper-bound argument is available in the accompanying repository.
Problem
The book Ramsey number R(B_8,B_10) was known to lie in the interval [37, 38], with the lower bound established but the exact value unsettled.
Approach
The proof rules out a 37-vertex graph containing neither B_8 nor a copy of B_10 in its complement. A counting argument via Goodman's identity forces any such graph to be 18-regular and strongly regular with parameters (37,18,7,10). A spectral argument then excludes the existence of such a strongly regular graph. The proof was discovered by AutoMath, an AI-assisted mathematical discovery tool, and formalized in Lean using GPT-5.5 Pro through Codex.
Results
R(B_8,B_10) = 37 is established. The Lean formalization of the upper-bound argument is publicly available.