Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
Benjamin Przybocki, John Mackey, Marijn J. H. Heule, Bernardo Subercaseaux
math.CO
Apr 23, 2026 · v1
TL;DR
Uses LLMs to generate and formalize correctness proofs in Lean for discovered infinite families of doubly saturated Ramsey-good graphs.
Abstract
Ramsey-good graphs are graphs that contain neither a clique of size $s$ nor an independent set of size $t$. We study doubly saturated Ramsey-good graphs, defined as Ramsey-good graphs in which the addition or removal of any edge necessarily creates an $s$-clique or a $t$-independent set. We present a method combining SAT solving with bespoke LLM-generated code to discover infinite families of such graphs, answering a question of Grinstead and Roberts from 1982. In addition, we use LLMs to generate and formalize correctness proofs in Lean. This case study highlights the potential of integrating automated reasoning, large language models, and formal verification to accelerate mathematical discovery. We argue that such tool-driven workflows will play an increasingly central role in experimental mathematics.
Problem
Grinstead and Roberts asked in 1982 whether infinite families of doubly saturated Ramsey-good graphs exist. A doubly saturated Ramsey-good graph contains neither an s-clique nor a t-independent set, and adding or removing any edge creates one.
Approach
The method combines SAT solving with bespoke LLM-generated code to discover infinite families of doubly saturated Ramsey-good graphs. LLMs are then used to generate and formalize correctness proofs of these constructions in Lean.
Results
The work answers the 1982 question of Grinstead and Roberts by presenting infinite families of doubly saturated Ramsey-good graphs. Correctness proofs are formalized in Lean, demonstrating the integration of automated reasoning, LLMs, and formal verification for mathematical discovery.
