---
name: Ramsey 数の Lean 4 形式化先行研究 (2024 CICM)
description: R(3,3)=6 は Narváez 2024 が Lean 4 で既に形式化済み、世界初は不可能
type: project
originSessionId: 80a567c3-c92a-4757-ac12-f814a062c754
---
Ramsey 数の Lean 4 形式化を計画する際、以下の先行研究を必ず引用する。

## 主要先行研究 (調べ済み 2026-04-21)

| 著者・年 | 系統 | 内容 |
|---------|------|------|
| **Narváez, Song, Zhang (CICM 2024)** | Lean 4 | "Formalizing Finite Ramsey Theory in Lean 4" — small Ramsey numbers + van der Waerden numbers の exact value 形式化。R(3,3)=6 を含む可能性が極めて高い |
| **Gauthier & Brown (ITP 2024)** | HOL4 | R(4,5)=25 の完全形式化 (arXiv:2404.01761) |
| **Mathlib4 本体** | Lean 4 | `ramseyNumber` 定義は **まだ無い** (formal-conjectures #2364 で good first issue) |
| **Heule (2017)** | ACL2/SAT | Schur S(5)=160 の SAT 証明、Lean 化はまだ |

DOI/URL:
- Narváez 2024: https://link.springer.com/chapter/10.1007/978-3-031-66997-2_6
- Gauthier-Brown HOL4: https://arxiv.org/abs/2404.01761
- DeepMind Ramsey issue: https://github.com/google-deepmind/formal-conjectures/issues/2364

**Why:** 2026-04-21、藤本さんが「Lean 4 機械検証世界初」を主張する前に正直確認を依頼。調査結果、R(3,3)=6 の Lean 4 形式化は**既に存在する**。Mathlib 本体には無いが学術文献にはあるため、honest に "world first" は主張不可。

**How to apply:**
- R(s,t)=N の Lean 4 形式化を主張する論文では Narváez 2024 と Gauthier-Brown 2024 を必ず引用
- "world first" ではなく以下のいずれかで打ち出す:
  - "Mathlib4 への最初の PR contribution" (formal-conjectures #2364 解決として)
  - "alternative `native_decide` mechanization" (Narváez らが手法を異にする場合)
  - "independent re-formalization in Mathlib v4.27"
- Schur/EGZ/W も同様の先行研究確認を必ず行う
- 主張前に WebSearch + GitHub 検索で必ず先行を調べる