Computer-Assisted Discovery of Doubly Saturated Ramsey Graphs

A recent mathematical paper released on arXiv introduces a technique that merges SAT solving with code generated by large language models (LLMs) to identify infinite families of doubly saturated Ramsey-good graphs. These specific graphs lack both an s-clique and a t-independent set, with the addition or removal of any edge resulting in one. This method addresses a query raised by Grinstead and Roberts back in 1982. Additionally, the researchers utilized LLMs to create and formalize correctness proofs within Lean. This study showcases how automated reasoning, LLMs, and formal verification can expedite mathematical exploration, suggesting that such tool-based approaches will play a pivotal role in experimental mathematics.