mlsanityData to 7 Oct 2026

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

arXiv 2604.21187 ↗First posted 23 Apr 2026math.CO cs.AIcited by 0

Not on the map. Why?

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.

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

Builds on

13 of 46 references.

References · 13

  1. 2019The Lean mathematical librarycited by 127
  2. 2024A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challengescited by 55
  3. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  4. 2025Early science acceleration experiments with GPT-5cited by 35
  5. 2026Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the ErdHos Problemscited by 24
  6. 2016Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquercited by 23
  7. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19
  8. 2026130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?cited by 16
  9. 2019The Resolution of Keller's Conjecturecited by 8
  10. 2026Solving an Open Problem in Theoretical Physics using AI-Assisted Discoverycited by 7
  11. 2023The Packing Chromatic Number of the Infinite Square Grid is 15cited by 4
  12. 2026Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Designcited by 2
1 more
  1. 2023Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Planecited by 1

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2026RamseyGadgets: A Graph Construction Dataset for LLMs
  2. 2025A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
  3. 2026ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics
  4. 2026Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science
  5. 2026Advancing Mathematics Research with AI-Driven Formal Proof Search
  6. 2026MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis
  7. 2025Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving
  8. 2026k-server-bench: Automating Potential Discovery for the k-Server Conjecture