用AI发现无限多类特殊图，解决数学界40年难题
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
- 结合SAT求解与LLM生成代码，自动搜索特殊图结构
- 首次构造出无穷多个双饱和拉姆齐图，验证1982年猜想
- 用LLM生成并形式化证明，推动数学发现自动化
拉姆齐好图是指既不含大小为s的团，也不含大小为t的独立集的图。本文研究双饱和拉姆齐好图，即任意增删一条边都会产生一个s-团或t-独立集的图。我们提出一种结合SAT求解与定制化LLM生成代码的方法，发现了此类图的无限家族，回答了Grinstead和Roberts于1982年提出的问题。此外，我们还利用LLM生成并形式化了正确性证明，使用Lean进行验证。本案例展示了自动化推理、大语言模型与形式化验证融合在加速数学发现中的潜力，论证了工具驱动工作流将在实验数学中扮演日益核心的角色。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。