{"id":"arxiv/2604.21187","url":"https://arxiv.org/abs/2604.21187","tags":["math.CO","cs.AI"],"score":0,"title":"Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery","domain":"math.CO","source":"arxiv","authors":["Benjamin Przybocki","John Mackey","Marijn J. H. Heule","Bernardo Subercaseaux"],"reviews":0,"subject":"math.CO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-23","reactions":{}}