二重飽和ラムゼーグラフ：数学発見におけるコンピュータ支援へのケーススタディ

arXiv:2604.21187v1 発表タイプ: cross 要旨：ラムゼー善なるグラフとは、サイズ $s$ のクライクおよびサイズ $t$ の独立集合をどちらも含めないグラフのことである。本稿では、辺の追加または削除が必ずサイズ $s$ のクライクまたはサイズ $t$ の独立集合を生じさせるラムゼー善なるグラフ、すなわち二重飽和ラムゼーグラフを対象とする。我々は、SAT 解法と LLM によって生成された特化コードを組み合わせた方法を提供し、1982 年に Grinstead と Roberts が提起した問いに対する答えを導出した。さらに、我々は LLM を用いて正解証明を生成し、Lean において形式化した。このケーススタディは、自動化された推論、大規模言語モデル、および形式検証を統合することによる数学的发现の加速の可能性を浮き彫りにした。我々は、そのようなツール駆動されたワークフローが実驗数学においてより中心的な役割を果たすようになるだろうと論じる。

arXiv:2604.21187v1 Announce Type: cross Abstract: 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.