18人の全員どうしを赤か青の線で結ぶと、どう塗っても、同じ色の「三角形が4つ1点でつながった形（扇）」が必ずできる。17人なら、できない塗り方がある。
この「必ずできる最小の人数」は扇のラムゼー数 R(F₄,F₄) と呼ばれていて、これまでは「17以上24以下」までしか分かっていませんでした。これを SAT ソルバーで 18 と確定させ、論文とデータを Zenodo で公開しました（査読はまだ受けていません）。
この記事では、論文（6ページ・英語）の中身を、プログラムを書く人向けに日本語で書き下します。数学の予備知識は要らないように書いたつもりです。探索のコード・計算・論文の初稿は、AIエージェント（Claude Code）と一緒に作りました（論文の謝辞にも書いています）。
ラムゼー数とは
6人を集めて、知り合いどうしを赤、他人どうしを青の線で結びます。すると、どう結んでも「3人とも知り合い」か「3人とも他人」、つまり同じ色の三角形が必ずできます。5人では、できない結び方があります（五角形の辺を赤、対角線を青にする）。
6人で必ずできる理由は短く言えます。1人に注目すると、残り5人への線が5本あるので、どちらかの色が3本以上あります。仮に赤が3本とすると、その3人のあいだの線が1本でも赤なら赤い三角形、3本とも青なら青い三角形です。
このように「n 人いれば、どう塗っても赤の G か青の H が必ずできる」最小の n を、ラムゼー数 R(G, H) と呼びます。K_n は n 人全員を線で結んだ形で、K₃ は三角形です。上の例は R(K₃, K₃) = 6。小さく見えても難しく、K₅ どうしの R(K₅, K₅) は 43〜46 までしか分かっていません。
扇 F_n と、これまで分かっていたこと
扇 F_n は、n 個の三角形が1つの頂点（中心）を共有した形です。頂点は 2n+1 個。F₁ はただの三角形です。
扇どうしのラムゼー数で、小さいものは次のとおりでした（Radziszowski の動的サーベイ「Small Ramsey Numbers」第18版、2026年4月と、その後の論文から）。
| 値 | 出典 | |
|---|---|---|
| R(F₁, F_n)（n≥2） | 4n+1 | Li–Rousseau 1996 |
| R(F₂, F₂) | 9 | Burr 1983 |
| R(F₂, F_n)（n≥2） | 4n+1 | Lin–Li 2009 |
| R(F₃, F₃) | 14 | Zhao–Wei 2022 |
| R(F₃, F₄) | 17 | Jiang–Shao 2026年10月 |
| R(F₄, F₄) | 17〜24 → 18 | この記事 |
R(F₄, F₄) の下限 17 は R(F₁, F₄) = 17 から、上限 24 は一般の不等式 R(F_m, F_n) ≤ 4n+2m から来ています。サーベイの表には、別の一般式から出る 28 だけが載っていました。
下からの限界：17人で扇を作らない塗り方
「18以上」を示すには、17人で扇を1つも作らない塗り方を1つ見せれば十分です。見つけた塗り方は、0と1の対称な表です（1が青、0が赤）。
0 01111111100000000
1 10111111011100000
2 11000000111011110
3 11000000100011101
4 11000000011011111
5 11000000011011011
6 11000000011010111
7 11000000011001111
8 10110000000011110
9 01101111001100010
10 01101111010100010
11 01000000011011111
12 00111110100100001
13 00111101100100001
14 00111011100100001
15 00101111111100000
16 00011111000111100
扇がないことは、次のように確かめられます。以下は記事のために書いた確認コードです（論文の確認に使った2つのプログラムとは別）。頂点 v を中心とする赤い F₄ は、「v と赤で結ばれた人たち」の中で、赤い辺を4本、互いに端点を共有せずに選べることと同じです。つまり、赤の近所の中の最大マッチングが3以下なら、v を中心とする赤い F₄ はありません。
import itertools, networkx as nx
def max_fan(mat):
"""各頂点・各色で、同じ色の近所の中の最大マッチングの大きさの最大値（F_k があるなら k 以上）"""
n, best = len(mat), 0
for v in range(n):
for c in "01":
nb = [u for u in range(n) if u != v and mat[v][u] == c]
G = nx.Graph(); G.add_nodes_from(nb)
G.add_edges_from((a, b) for a, b in itertools.combinations(nb, 2) if mat[a][b] == c)
best = max(best, len(nx.max_weight_matching(G, maxcardinality=True)))
return best
M = open('colouring_F4F4_K17.txt').read().split() # 17行の0/1の文字列（Zenodo のデータに入っています）
assert max_fan(M) == 3 # 17人・2色の全部で3以下 → F4 は無い
論文では、この確認を別々に書いた2つのプログラムで行い、どちらもでたらめな塗り方なら F₄ を見つけることを確かめています。なお、対称性の高い「巡回型」の塗り方では、扇を避けられるのは16人までで、17人の例は巡回型ではありません。
上からの限界：18人なら必ずできる
ここが本題です。18人の線は153本あり、塗り方は 2¹⁵³ ≈ 1.1×10⁴⁶ 通りあります。全部を試すことはできないので、次の3段階で問題を小さくしてから、SAT ソルバーに「どの塗り方でも扇ができる」ことを示させました。
- 手で示せる事実で、1人から出る同じ色の線の本数（色の次数）を11本以下に絞る
- 色の次数の最大値 D で、場合を D = 9, 10, 11 の3つに分ける
- 人の番号の付け替えで同じになる塗り方を、辞書順の条件で1つにまとめる（対称性の除去）
1. 色の次数は11本以下
「12人をどう塗っても、赤の 4K₂（端点を共有しない赤い辺4本）か、青の F₄ ができる」という事実を使います。これは R(nK₂, F_n) = 3n の n=4 の場合で、論文ではこれも SAT で独立に確かめました。
もし誰かが赤の線を12本以上持っていたら、その12人の中に赤の 4K₂ か青の F₄ があります。青の F₄ は扇そのもの。赤の 4K₂ は、その人を中心にすれば赤の F₄ です。どちらでも扇ができるので、扇のない塗り方では、どの人の赤の線も青の線も11本以下です。
2. 最大の色の次数で場合分け
18人なら1人から出る線は17本なので、赤か青のどちらかは9本以上です。そこで、全員・両方の色の中で最大の色の次数を D とすると、D は 9, 10, 11 のどれかです。
色を入れ替え、番号を付け直せば、次の形を仮定できます。
- (N1) 0番の人は、1〜D番と赤で、D+1〜17番と青で結ばれている
- (N2) どの人も、赤の線の本数は 17−D 以上 D 以下（赤も青も D 本以下で、青の本数＝17−赤の本数だから）
3. ブロックの中の辞書順で対称性を除く
番号を付け替えただけの同じ塗り方を何度も調べると、計算が終わりません。そこで、塗り方を隣接行列（赤=1）として見たとき、次の条件を足します。
- (N3) 同じブロック（1〜D番、または D+1〜17番）の i < j について、i 行目と j 行目を、i 列と j 列を除いて比べると、辞書順で i 行目 ≤ j 行目
この形の条件は Codish・Miller・Prosser・Stuckey（2019）が全体の並べ替えについて導入したものです。今回は (N1) を崩さないように、0番を動かさず、ブロックの中だけで並べ替える版にしました。そのため、取りこぼしがないことの証明を論文に書いています。
考え方は次のとおりです。ブロックの中の並べ替えで移り合う塗り方のうち、行列の上三角を行ごとに読んだ文字列が辞書順で最小のものを選びます。もしそれが (N3) を破る i < j を持っていたら、i と j を入れ替えてみます。同じブロックの中の入れ替えなので、(N1)・(N2) も、扇がないことも崩れません。i 行目と j 行目が初めて食い違う列を c とすると、入れ替えで文字列の中で最初に変わるのは i と c の組の値で、そこが 1 から 0 になります。つまり文字列がもっと小さくなり、最小に選んだことと矛盾します。だから、最小のものは必ず (N3) を満たします。
SAT への書き下し
SAT ソルバーは、「真か偽の変数」と「どれか1つは成り立て」という節（CNF）の集まりを渡すと、全部の節を満たす割り当てを探し、なければ「解なし（UNSAT）」と答える道具です。
変数は、辺 uv が赤なら真になる x_uv（153個）と、三角形 abc が色 γ のときに真になるよう強制する補助変数 t_γ,abc です。
¬x_ab ∨ ¬x_ac ∨ ¬x_bc ∨ t_0,abc （3辺とも赤なら t_0,abc は真）
x_ab ∨ x_ac ∨ x_bc ∨ t_1,abc （3辺とも青なら t_1,abc は真）
中心 v と、4本の辺 a₁b₁, …, a₄b₄ でできる色 γ の扇は、「4つの三角形のどれかは色 γ でない」という節で禁止します。
def fan_clause(self, c, v, sel):
return [-self.t(c, v, a, b) for a, b in sel]
(N2) の本数の条件は PySAT の逐次カウンタ（EncType.seqcounter）で、(N3) の辞書順は「ここまで等しい」を表す補助変数を1つずつ足す標準の書き方で入れます（以下のコードは、実物から要点だけを残して短くしたものです）。
def add_lex_le(self, A, B):
"""A <=lex B for equal-length lists of literals (False<True)."""
e_prev = None
for i, (a, b) in enumerate(zip(A, B)):
# ここまで等しければ a <= b
self.clauses.append([-a, b] if e_prev is None else [-e_prev, -a, b])
if i == len(A) - 1:
break
e = self.new()
if e_prev is not None:
self.clauses.append([-e, e_prev])
base = [] if e_prev is None else [-e_prev]
self.clauses.append(base + [a, b, e]) # (ここまで等しい かつ a == b) → e
self.clauses.append(base + [-a, -b, e])
e_prev = e
扇の節は、必要な分だけ後から足す
18人の扇の節を全部書き出すと膨大になります。そこで、最初は扇の節なしで解かせ、出てきた塗り方の中で同じ色の F₄ を探し、見つけたものだけを節として足して、また解かせます。これを「解なし」になるまで繰り返します（これも要点だけに縮めています）。
while True:
if not S.solve():
res = 'UNSAT'; break
M = P.colour_matrix(S.get_model())
added = 0
for c in (0, 1):
for v in range(P.N):
nb = [u for u in range(P.N) if u != v and M[v][u] == c]
E = [(x, y) for x, y in itertools.combinations(nb, 2) if M[x][y] == c]
for sel in k_matchings(E, 4, cap, rng): # 中心 v の F4 を最大200個まで
cl = P.fan_clause(c, v, sel)
if tuple(sorted(cl)) not in P.fanset:
P.fanset.add(tuple(sorted(cl))); S.add_clause(cl); added += 1
if not added:
res = 'SAT'; break # 扇のない塗り方が見つかった（18人ではこうならなかった）
最後の論理式に入っているのは本物の扇の節だけなので、それが「解なし」なら、扇の節を全部入れた論理式も「解なし」です。
結果
最後の論理式を CaDiCaL 2.1.3 で解き、LRAT 形式の証明を出させました。
| 論理式 | 変数 | 節 | 扇の節 | LRAT | 解く | 検査 |
|---|---|---|---|---|---|---|
| 次数の補題（12人） | 1,100 | 13,853 | 8,107 + 2,930（青の F₄ ＋ 赤の 4K₂） | 0.13 MB | 2 s | 1 s 未満 |
| D = 11 | 5,079 | 122,598 | 112,431 | 11.8 MB | 7 s | 4 s |
| D = 10 | 5,155 | 327,202 | 316,935 | 223 MB | 100 s | 65 s |
| D = 9 | 5,193 | 450,041 | 439,690 | 1.04 GB | 749 s | 196 s |
扇の節を後から足していく段階には、D = 11, 10, 9 でそれぞれ9秒・143秒・1,321秒かかりました。時間はどれもデスクトップ PC の1コアでの実測です。
3つの場合がすべて「解なし」なので、18人のどんな塗り方にも同じ色の扇があります。下からの限界と合わせて、R(F₄, F₄) = 18 です。
正しさをどう確かめたか
計算機による証明でいちばん疑われるのは、「ソルバーやエンコードに誤りはないか」です。次の層で確かめています。
1. 証明を、検証済みのチェッカーで検査した
「解なし」の主張にはすべて LRAT 形式の証明ファイル（ソルバーが「解なし」に至った推論を1歩ずつ記録したもの）を付け、cake_lpr で検査しました。cake_lpr は、機械語の実装まで CakeML で形式的に検証された検査器です。4つとも s VERIFIED UNSAT で通っています。これで「ソルバーの答えが正しいか」は、ソルバーを信じなくても確かめられます。
2. 論理式が正しい問題を表しているかを、別のプログラムで読み直した
検査器が保証するのは「この論理式は解なし」までです。論理式そのものが正しく作られているかは、別に書いたプログラムで3つの CNF ファイルを読み直して確かめました。三角形の変数を含む節が、正しい符号の定義の節か、「同じ色の4つの三角形が1点だけを共有し、9つの別々の頂点を覆う」扇の節のどちらかであること。変数が1つだけの節（単位節）が、ちょうど (N1) の17本であること。扇でない節をわざと1つ混ぜると、この検査が見つけることも確かめています。
3. 対称性の除去が取りこぼさないことを、小さい場合で総当たりした
6人以下は全部の塗り方、7人はでたらめな300通りについて、許した付け替えで (N1)〜(N3) の形に持っていけることを確かめました。辞書順の条件だけでも、4・5・6頂点のグラフの同型の類（11・34・156類）を1つずつ残すことを確かめています。
4. 同じコードで、知られている値を再現した
R(K₃,K₃)=6、R(F₂,F₂)=9、R(F₂,F₃)=13、R(F₃,F₃)=14、R(F₂,F₄)=17 を再現できました。
5. ついでに R(F₃, F₄) = 17 を別の方法で確かめた
場合分けをしない17人の論理式（842 MB の LRAT）と、348個に分けて解く方法（cube-and-conquer。すべての分け方を覆うことも検査）の2通りで「解なし」を確かめ、どちらも cake_lpr で検査しました。Jiang–Shao の結果を、別の方法で独立に裏づけたことになります。
補足：辞書順の条件を外すと
ブロックの中の辞書順の条件を外して解かせると、扇の節が200万本を超えても、決めた時間内には収束しませんでした。結果の正しさは、上の取りこぼしのなさの証明と、エンコードの検査の両方に支えられています。
再現の仕方
Zenodo に、塗り方・最後の4つの CNF ファイル（SHA-256 付き）・論理式を作るスクリプト・検査のログを置いています。LRAT 証明は合わせて 1.3 GB あるので入れていませんが、CaDiCaL 2.1.3 で CNF から同じものを作り直せます。
# cadical（rel-2.1.3）と cake_lpr が PATH にある環境で
code/lrat_verify.sh cnf/F4F4_N18_D9.cnf # D10, D11, deg_4K2_F4_K12 も同じ
python code/fan_v0.py 4 18 11 --cnf F4F4_N18_D11.cnf # 論理式を作り直す（D = 10, 9 も）
18人と17人の境目
18人の全員を2色で結ぶと、同じ色の扇（三角形4つ）が必ずでき、17人なら避けられます。上からの限界は、色の次数の上限・最大の色の次数での場合分け・ブロックの中の辞書順という3段階で問題を小さくし、SAT ソルバーで3つの場合をすべて「解なし」にして示しました。証明はすべて検証済みのチェッカーで確かめてあり、データは誰でも検算できます。
同じやり方がもっと大きい扇（R(F₄, F₅) など）に届くかは、まだ試していません。