未解決問題への挑戦
「17〜24のどこか」とまでしか分かっていなかった数や、研究者の表で空欄のままだった値を、SAT ソルバーで決めています。答えには必ず、だれでも確かめ直せる証拠を付けます。下の結果は論文とデータを Zenodo で公開していますが、まだ査読を受けていません。
2026年10月25日 公開
18人の全員どうしを、赤か青の線で結びます。どう塗っても、同じ色の「扇」（1人を中心に、三角形が4つつながった形）が必ずできます。17人だと、扇を1つも作らない塗り方があります。だから答えは 18 です。
17人の側は、扇のない塗り方を1つ見せれば済みます。18人の側は、塗り方が 2153 通りあって全部は試せません。そこで「1人から出る同じ色の線は11本まで」と分かることなどを使って3つの場合に分け、SAT ソルバーに「そんな塗り方はない」と示させました。その証明ファイル（合わせて1.27GB）を、正しさが数学的に保証された検査器 cake_lpr で1行ずつ確かめています。
あわせて、2026年10月に Jiang・Shao が発表した R(F₃, F₄) = 17 も、別の方法で確かめました。
2026年10月28日 公開
1から n までの整数を4色で塗ります。n が 313 なら、どう塗っても、同じ色の x, y, z で 4(x−y) = 3z になる組が必ずできます。312 までなら避けられます。この「必ずできる最小の n」がラドー数です。
2022年に Chang・De Loera・Wesley がまとめた4色の値の表（論文の表10）で、空欄だった2つです。625 は 5 の4乗とちょうど同じで、「a ≥ b+2 なら答えは a⁴」という3色で知られた形が4色でも成り立つかもしれない、という手がかりになります。
確かめ方は扇と同じです。下の側は実際の塗り方を別のプログラムで検査し、上の側は証明ファイルを cake_lpr で検査しました（大きい場合は問題を数千の小部分に分け、分け方に漏れがないことも検査）。手順に頼る部分を減らすため、313 と 625 は「色の入れ替えで同じになる塗り方を省く」工夫を外した式でも確かめています。
| 値 | 先に出した人 | こちらでしたこと |
|---|---|---|
| R(F₃, F₄) = 17 | Jiang・Shao（arXiv:2610.26109、2026年10月19日） | 扇の計算と同じ道具で、場合分けをしない式と、細かく分けて解く方法の2通りで確かめた |
| R₄(2(x−y)=3z) = 226 | Ichikawa（Zenodo、2026年10月22〜23日） | 7月に計算を終えていたが、公開は先方が先。先方が弱点に挙げていた2点（工夫を外した式での確認、検証済みの検査器）を埋める形で確かめた |
226 は、計算が終わってから3か月寝かせているあいだに先を越されました。この経験から、扇の R(F₄, F₄) は計算を終えた翌日に公開しました。
「どの頂点からも3本以上の線が出ているグラフには、長さが 4, 8, 16, … （2の累乗）のどれかの輪が必ずある」という予想です。反例が1つ見つかれば決着します。
各頂点からちょうど3本ずつ線が出るグラフに絞って探し、SAT ソルバーでは 32頂点まで反例はないという答えになりました。ただし、証明ファイルを出して別の検査器で確かめてはいないので、「確定」とは書きません。焼きなまし法でも、長さ16の輪だけがどうしても消えませんでした。反例が出なければやめると決めていたので、ここで打ち切りました。
| 問題 | いま分かっている範囲 | 決まったら載る場所 |
|---|---|---|
| 本のラムゼー数 R(B₄, B₇) | 22〜23（差は1） | ラムゼー数の一覧（Radziszowski の Dynamic Survey） |
| 扇のラムゼー数 R(F₃, F₅) | 21〜26 | 同上。扇の計算の道具がそのまま使える |
| Tao らの「最適化定数」の一覧 | 90番まで（約120項目）の定数の上下の限界 | Davis・Ivanisvili・Tao が管理。改善すると、更新の欄に改善した人の名前つきで載る |
探索のコード、計算の実行、論文の下書きは、AI エージェント（Claude Code）と一緒に作りました。論文の謝辞にもそう書いています。AI が出した答えをそのまま信じないために、上の「確かめ方」の4段を、どの結果にも必ず通しています。