2026年7月15日、Redditの数学板に地味なタイトルの投稿が現れた。要するに「OpenAIのCDC予想の証明手法を見て、GPT-5.6で試してみたら、30年空いていた穴を塞いだ」という内容だった。
三日後、この投稿はHacker Newsで477のアップボートと308件のコメントを集めた。Leanのコードを一行ずつ読んだ数学者たちの態度は、意外なほど一致していた：今回のは本物の数学的貢献だ。
筆者が議論を一通り読んで感じたのは、この件の衝撃の正体が、人間の数学者でさえ特に手強いと感じるタスク——「下界を証明すること」——に触れたという点だ。そしてGPT-5.6はプロンプト1つ、148分でそれをやってのけた。
何が起きたか：プロンプト1つ、148分、30年の空白
Phillip KergerはUC Berkeleyの応用数学助教授で、Johns Hopkinsで最適化理論の博士号を取り、以前はNASAの量子人工知能研究所で研究していた。昨年から断続的に一つの問題に取り組んでいた——凸最適化の分野で1996年以来未解決だった複雑さの空白だ。
簡単に言うと：1996年に誰かが設計したアルゴリズムの複雑さは \(O(d^2 \log^2 d)\) だった。誰もが \(O(d)\) より良くなることはありえないと知っていた（少なくとも各次元を一度は見なければならないからだ）。しかし \(O(d)\) から \(O(d^2 \log^2 d)\) の間の30年間の空白を埋められる者はいなかった——「もっと速くできるのか、それともその古いアルゴリズムがすでに限界なのか？」
Kergerは以前GPT-5.4とGPT-5.5を試したが、どちらも失敗した。正しい関数族へ思考を向けさせても、最後の数ステップを模型は補えなかった。
そしてGPT-5.6が来た。
彼はOpenAIが数週間前に公開した「循環二重被覆予想（cyclic double cover conjecture）」の証明プロンプトの構造を参考に、約10ページのプロンプトを書いた——その中には数学的な設定、考えられる証明のルートの列挙、自分のこれまでの失敗した試みの経験、そして「どんな結果なら有効解とみなさないか」の明確な定義が含まれていた。彼はまずGPT-5.6を使って関連文献を整理し、プロンプト内の議論の枠組みを整え、それから一つの連続したセッションで最終版を模型に与えた。
148分後、GPT-5.6は完全な証明の構成を吐き出した。
画像出典：Unsplash / GuerrillaBuzz — 凸最適化手法の収束性を示す図。GPT-5.6が証明したのは、下界の曲線をこれ以上押し下げられない——1996年の古いアルゴリズムはすでに理論的限界に乗っているということだ。
結果は：\(\Omega(d^2 / \log(d+1))\) の下界で、既知の上界 \(O(d^2 \log^2 d)\) との差は対数因子だけになった。これは「あの30年の古いアルゴリズムよりずっと速い方法が存在する」という可能性を排除する。
なぜ「下界を証明する」のはずっと難しいのか？走ることで例える
この件の重みを理解するために、筆者は身近な比喩を一つ挙げる。
上界を証明するのは、100メートル走れることを証明するようなものだ——一度走って、タイマーを押せば、結論は成り立つ。
下界を証明するのは、あなたが「それ以上速く走れない」ことを証明するようなものだ——そのためには考えられるすべてのトレーニング方法を排除しなければならない。シューズを変える？無駄だ。スタートの姿勢を変える？無駄だ。特別な食事？やはり無駄だ。「あなたは9秒を切れない」という結論を成立させるには、想像しうるすべての方法を挙げ、一つずつそれらが役に立たないことを証明しなければならない。
数学において、上界を証明する（「この程度まではできるという方法を見つけた」）のは比較的容易だ——アルゴリズムを一つ与え、その複雑さを計算すれば終わりだ。しかし下界を証明する（「これより速い方法はどんなものも存在しない」）には、「ありうるすべてのアルゴリズム」を拘束しなければならない。あなたは証明しなければならない：他人がどんな新しいアルゴリズムを設計しようと、どんな技巧を使おうと、どれだけ遠回りしようと——すべて無駄で、限界はここにある、と。
だからHNで alternator と名乗る、「この分野を少しは知っている」と自称するコメンテーターはこう言ったのだ：
“Proving an upper bound is easy — it’s just how long your algorithm takes to run. Proving a non-trivial lower bound is much harder, because it requires you to constrain all possible algorithms.”
そしてGPT-5.6が今回やったことは、まさに後者だ。それはKergerが構成したアルゴリズムが優れていることを証明しただけではない——それが証明したのは、「あの1996年の古い手法がすでに理論的天井に達している」ということだ。30年間、誰も「もっと良いやり方があるかもしれない」という可能性を排除できなかったが、GPT-5.6は148分でそれを排除した。
二つの「AIが数学をする」：もう混同しないでほしい
AIが数学をする話をする際、二つのことを区別する必要がある。見かけは似ているが、本質的に全く異なる。
第一のパターン：AIによる推測の補助。 これはすでに何年も前から起きていることだ。研究者は模型に既知の結果の間のパターンを見つけさせ、「有望に見える」予想を生成させ、そして人間が検証する。模型が「この不等式は成り立つ気がする」と言い、人間が紙とペンかコンピュータでチェックする。このシナリオではAIは非常に賢い助手だが、最終的な判断は人間にある。
第二のパターン：AIが厳密な証明を自立的に完成させ、形式検証を通過すること。 これがGPT-5.6が今回やったことだ。模型が出力したのは「もっともらしい」議論だけではない——その議論はLean 4という数学証明支援システムに丸ごと翻訳され、行ごとにコンパイルを通過したのだ。Leanは「明らかに従う」「容易にわかる」といった修辞を受け付けない。Leanの世界では、すべてのステップの論理が完璧か、さもなくばエラーになるかの二者択一で、中間はない。
Kergerは証明全体のLeanコードをGitHubに置いた。 elan というバージョン管理ツールをインストールし、リポジトリをクローンして、一行 lake build を実行すれば、誰でもコンパイラが最初から最後までエラーを出さないことを目の当たりにできる。さらに #print axioms を実行して、 sorryAx （Leanで「このステップはまだ証明していない」を示すプレースホルダー）がないことを確認する——これは、論理の連鎖全体に穴がないことを意味する。
Kergerの36ページのプレプリント、完全なプロンプト、模型との対話記録、Leanコード、ビルドの手順——すべて公開されている。この開示の水準は、謝辞に「AIシステムの助けに感謝」と一言書くだけの論文よりもずっと高い。
画像出典：Unsplash / Bozhin Karaivanov — Lean証明支援のコード画面。GPT-5.6の証明はLean 4に丸ごと翻訳されコンパイルを通過し、論理の連鎖全体に sorry （未証明ステップ）は一つもない。
公平を期して言えば：疑問の声もまた聞くに値する
筆者はこの記事を「AIが人間をねじ伏せた」という爽快感だけの話にしたくない。r/mathでもHNでも、理性的な疑問は少なくない。これらの声は、この件の全体像を理解する上で重要だ。
第一に、この分野は確かにニッチだ。 複数のコメンテーターが指摘するように、この凸最適化の下界問題の知名度は、OpenAIが以前解いた「循環二重被覆予想」よりもるかに低い。後者は50年 graph theory にぶら下がっていた有名な問題だが、この下界予想は比較的小さな最適化理論のコミュニティで主に活発だった。その学術的価値は本物だが、「枠を超える」程度は限られている。
第二に、転移可能性が疑わしい。 下界を証明するのに必要な推論パターン——ありうるすべてのアルゴリズムを拘束すること——は確かに難易度の高いカテゴリであり、GPT-5.6はこれについて能力を示した。しかしこの能力が凸最適化から他の数学分野へ転移するかは、現時点で誰も知らない。
第三に、優先権の争い。 r/mathの議論では、1990年代のロシア語の最適化文献をあさり、Kergerの証明の中心的補題はすでにソ連の数学者によって発表されているのではないかと疑う者がいた。ただ、西側のデータベースにあまり収録されていないジャーナルに載っていただけかもしれない。これが確認されれば、GPT-5.6の貢献は「ほとんど忘れ去られた文献から議論を再構築し、誰も使ったことのないやり方でそれを形式化した」というものになる。この二つの貢献の重みは異なる。
第四に、「148分」はすべてではない。 Kergerはこの問題にすでに1年間断続的に取り組んでいる。あの10ページのプロンプトには、問題への理解、失敗した試み、除外した行き止まりが詰め込まれていた。GPT-5.6の前に、GPT-5.4とGPT-5.5は同じ問題で失敗している。148分は最後の中断なしの証明探索——ゼロからの魔法ではない。RuntimeWireの報道が言うように：「プロンプトの中には1年分の分野の仕事が包まれている。」
画像出典：RuntimeWire / Gemini — AI生成の数学証明フローイラスト。覚えておくべきは：プロンプトの背後には1年分の分野の蓄積があり、148分は最後のステップの探索時間にすぎないということだ。
本当に重要なのはこの働き方だ
議論を脇に置いて、筆者がこの件で最も注目すべきだと思うものは、その具体的な定理そのものではない。
人 + AI + 形式検証という三角ワークフローが、再現可能であることが証明されたのだ。
Kergerのやり方は明快だ：大きな問題を小さな補題に分解し、各補題をまずLeanの厳密な文に翻訳してから、模型に証明を埋めさせる。コンパイルを通らない補題があれば、その補題だけを個別に反復する——一箇所の変更で証明全体が崩れ去ってやり直し、ということはない。このフローにフィールズ賞受賞者である必要はない。ハードルは：自分の問題を正確に定義できるか、という点にある。
言い換えれば、AIは「中程度の難易度」の数学問題を食べていく道すじに、すでに実践的なレシピを持っている。 これで数学者が失業するわけではない——問題を定義し、プロンプトを組み、出力がたわごとかを見極めることは、現時点ではやはり人間がやる。しかしそれは数学研究の日常を変えるだろう：研究者はますます演出家のように、AIはますます実行チームのようになる。
一人のHNコメンテーターが率直に言った：こうした議論を読むと、まるで何が書いてあるか分からない難解な書物を見ているような気分になる、と。しかし専門用語に怯えるな——この件の本質は単純だ。30年間、人間はあるアルゴリズムがどれだけ速く走れるかは知っていたが、「これが限界だ」とは言えなかった。一人のAIが、1年分の分野の蓄積で導かれて、148分で「これが限界だ」を証明した。 そして、Leanという別の機械がその課題を行ごとにチェックし、近道をしていないことを確認した。
これこそが2026年の数学の最前線だ——人、AI、そして証明コンパイラが、一つのプロジェクトチームで共働き始めている。
参考リンク：
- Reddit r/math: After OpenAI’s CDC proof announcement, GPT-5.6 used a prompt to close a 30-year gap in convex optimization
- HN 討論 (item?id=48957779)
