【geek-terminalニュース】W(2;3,21)=416をLean 4で検証したとの報告、保証の範囲を追う

【事象の全貌と背景】
「416個まで並べると、もう逃げ場がない」。Redditのr/MachineLearningで、van der Waerden数W(2;3,21)=416をLean 4で検証したという報告が登場した。投稿者u/Rodriguez909は、Kullmannが2010年に予想した値だと説明している。ただし、提供された公式・大手メディアの確認資料には、この成果を裏付ける記述がない。本稿では予想解決の確定ニュースではなく、検証資料を提示した投稿者の主張として扱う。[原投稿](https://www.reddit.com/r/MachineLearning/comments/1xivpue/w2321_416_a_van_der_waerden_number_conjectured_by/)

主張の内容は明快だ。1から416までの整数を赤と青にどう塗り分けても、赤い3項等差数列か青い21項等差数列が現れる。一方、1から415までなら両方を避ける塗り分けが存在するという。この二つがそろって、境界値が416だと言える。「数論予想」という紹介だが、焦点は整数の彩色を扱う組合せ論、ラムゼー理論の具体的問題だ。

面白さは、巨大な計算を伴う結論を、他人がどこまで追試できる形にしたかにある。投稿は、今年もDeepMindのFormal Conjecturesで未解決扱いだったと述べるが、その履歴まで本稿で独立確認したわけではない。今回の公開時期を可能にした計算資源や開発上の突破口も、提示情報からは特定できない。

【技術的ディープダイブ】
投稿者が挙げる規模は209ケース、38,661,140個の末端論理式。証拠パッケージは13.6GBだという。さらに、各反駁を「cake_pr」で検査し、そのファイルとLeanの項をダイジェストで結び付けたと説明する。これらは投稿上の仕様であり、編集部が全件を再実行した結果ではない。

この種の問題をSATに符号化するなら、各整数の色を真偽値に対応させ、禁止する等差数列ごとに制約を作る、という見方ができる。416について制約全体が充足不能なら、逃げ切れる彩色がないことに対応する。415では具体的な彩色が証人になる。ただし、これは主張を理解するための一般的な説明であり、今回の実装の符号化や分割アルゴリズムを確認した説明ではない。

Leanのカーネルが扱うのは、形式化された定理文に対する証明項だ。公式の検証ガイドも、定理文が意図した数学と対応するか、依存する公理が何かを確認する必要を説明している。外部で検査した充足不能性がLean側にどう接続されるかが、今回の核心になる。「外部チェッカーが受理した」と「計算を含む全体がLeanのカーネル内で証明された」は、保証の範囲を調べてから評価したい。[Lean公式ガイド](https://lean-lang.org/doc/reference/latest/ValidatingProofs/)

特に、仮に定理が「全ケースが充足不能なら結論が従う」という条件付きなら、その条件を誰がどう満たしたかが残る。公理一覧の確認だけでは、定理の引数として置かれた仮定の解消まで分からない。ケース分割の網羅性、整数区間の端点、等差数列の公差の条件も、定理文と実装を突き合わせる対象になる。

名称にも確認点がある。投稿の表記はcake_prだが、CakeML公式が紹介するCNF充足不能性の検証器はcake_lprだ。同じ実装を指す表記揺れか、別の構成かは未確認。検証済みチェッカーの存在を根拠に、今回の接続まで自動的に正しいとは言えない。[CakeML公式](https://www.cakeml.org/checkers.html)

【コミュニティの生々しい熱量と議論】
確認できる肉声は、まず投稿者本人のものだ。「nothing counted unless the Lean kernel or cake_pr accepted it」――Leanのカーネルかチェッカーが受理しなければ成果に数えない、という姿勢を打ち出している。派手な解答文より、受理可能な証拠を前面に出す。この宣言には、形式証明好きが反応する理由がある。

ただし、取得できた原投稿にはコメント本文が表示されず、提供資料にも第三者の発言はない。「研究者が絶賛」「懐疑派が炎上」といった反響は確認できない。賛否の人数や現場の合意を作り足すことはできず、ここで追える熱量は投稿者の説明までだ。

その説明で最も手触りがあるのは、証拠をダウンロードし、shasum -a 256 -c SHA256SUMSを実行せよという案内だ。ただし、チェックサムが確かめるのは、基準となる一覧とファイルのハッシュ値が一致すること。数学的正しさの検証や証明の再実行とは役割が違う。投稿者はLeanソース、検査記録、再実行キットを含むと説明するが、本稿ではパッケージ本体を取得・検証できていない。[投稿者提示の証拠パッケージ](https://doi.org/10.5281/zenodo.23749222)

また、生成にはHupyyのLPM、Large Proof Modelというニューロシンボリックシステムを使ったという。しかし、モデル構成、学習条件、人間の介入量、証明探索と形式化の分担は不明だ。この報告だけから「AIが自律的に予想を発見し、証明した」とは評価できない。

【今後の展望とエコシステムへの影響】
独立した再検証が成立すれば、注目点は416という一つの値に加え、大規模な有限計算をレビュー可能な成果物として渡す工程になる。探索する側と検査する側の役割を明確にし、第三者が定理文、証明、計算記録を追えるなら、AIを使った数学の評価を具体化できるだろう。

次に確認したいのは、415の彩色証人、416の上界証明、209ケースの網羅性、外部証明書との接続、そして別環境での再実行結果だ。これは既に専門家の追認が得られたという意味ではなく、成果の確度を上げるために残る確認事項である。

現時点で数学者や既存の証明手法が「オワコン」になったと言える根拠はない。もしこの方式が再現可能だと示されれば、変わり得るのは成果の見せ方だ。「解けた」という宣言に、何を仮定し、どのプログラムが何を検査したかという監査可能な記録を添える。その文化が広がるかどうかまで含めて、今回の報告を追う価値がある。