이중 포화 램지 그래프: 컴퓨터 지원 수학적 발견 사례 연구

Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery

램지 좋은 그래프는 크기가 $s$인 완전 그래프(클리크)도 크기가 $t$인 독립 집합도 포함하지 않는 그래프입니다. 본 연구에서는 어떤 간선이 추가되거나 제거될 때 항상 크기 $s$인 완전 그래프 또는 크기 $t$인 독립 집합이 생성되는 램지 좋은 그래프인, 이중 포화 램지 좋은 그래프를 연구합니다. SAT 해결과 맞춤형 LLM(대규모 언어 모델)이 생성한 코드를 결합하는 방법을 통해 이러한 그래프의 무한 가정을 발견하고, 1982년 Grinstead와 Roberts가 제기한 질문에 대한 답을 제시합니다. 또한, LLM을 사용하여 Lean에서 정확성 증명을 생성하고 형식화합니다. 이 사례 연구는 자동 추론, 대규모 언어 모델, 형식 검증을 통합하여 수학적 발견을 가속화할 수 있는 잠재력을 보여줍니다. 이러한 도구 기반 워크플로우가 실험 수학에서 점점 더 중요한 역할을 할 것이라고 주장합니다.

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.