# Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery

arXiv: https://arxiv.org/abs/2604.21187 · HTML: https://mlsanity.com/paper/2604.21187/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 46 references that are in the map.
- First posted on arXiv 23 Apr 2026.

## Builds on (most cited first, 13 of 13)

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challenges](https://mlsanity.com/paper/2412.11936/) (2024)
- [Early science acceleration experiments with GPT-5](https://mlsanity.com/paper/2511.16072/) (2025)
- [Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the ErdHos Problems](https://mlsanity.com/paper/2601.22401/) (2026)
- [Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer](https://mlsanity.com/paper/1605.00723/) (2016)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [The Resolution of Keller's Conjecture](https://mlsanity.com/paper/1910.03740/) (2019)
- [Solving an Open Problem in Theoretical Physics using AI-Assisted Discovery](https://mlsanity.com/paper/2603.04735/) (2026)
- [The Packing Chromatic Number of the Infinite Square Grid is 15](https://mlsanity.com/paper/2301.09757/) (2023)
- [Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design](https://mlsanity.com/paper/2603.08322/) (2026)
- [Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane](https://mlsanity.com/paper/2311.03645/) (2023)

## Abstract (arXiv)

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.