arXiv ID:
2604.21187
arXiv 提交日期: 2026-04-23
双重饱和拉姆齐图:计算机辅助数学发现的一个案例研究 / Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
1️⃣ 一句话总结
本文通过结合SAT求解器和定制化大语言模型生成的代码,发现了无限族“双重饱和拉姆齐图”(即既不含指定大小的团也不含独立集,且增减任一边都会破坏这一性质),从而解决了1982年提出的一个数学问题,并展示了利用大语言模型自动生成并形式化证明(Lean)来加速数学发现的新方法。