双重饱和的Ramsey图：计算机辅助数学发现的一个案例研究
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
AI总结：
本文通过结合SAT求解与定制生成的代码，发现无限多的双重饱和Ramsey图，回答了Grinstead和Roberts在1982年的疑问，并利用LLM生成形式化证明，展示自动化推理、大语言模型和形式验证在数学发现中的潜力。
摘要：
Ramsey-good graphs是既不含s-clique也不含t-independent set的图。我们研究双重饱和的Ramsey-good graphs，定义为在添加或删除任何边时必然产生s-clique或t-independent set的图。我们提出一种结合SAT求解与定制生成代码的方法来发现无限多样的此类图，回答了Grinstead和Roberts在1982年的疑问。此外，我们使用LLM生成并形式化正确性证明。本案例研究展示了自动化推理、大语言模型和形式验证在加速数学发现中的潜力。我们主张此类工具驱动的工作流程将在实验数学中扮演越来越重要的角色。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
