Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917430441279488 |
|---|---|
| author | Przybocki, Benjamin Mackey, John Heule, Marijn J. H. Subercaseaux, Bernardo |
| author_facet | Przybocki, Benjamin Mackey, John Heule, Marijn J. H. Subercaseaux, Bernardo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_21187 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery Przybocki, Benjamin Mackey, John Heule, Marijn J. H. Subercaseaux, Bernardo Combinatorics Artificial Intelligence 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. |
| title | Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery |
| topic | Combinatorics Artificial Intelligence |
| url | https://arxiv.org/abs/2604.21187 |