【geek-terminalニュース】GPT-5.6 SolのLean検証つき凸最適化“30年ギャップ”主張を深掘り

【事象の全貌と背景】
以前お伝えしたGPT-5.6 Solによる数学証明騒動の続報です。前回の中心は、OpenAIのGPT-5.6 Sol Ultraが64のサブエージェントを使い、Cycle Double Cover Conjecture、いわゆるCDC予想の証明を1時間未満で生成したとされる話でした。ただしこのCDC証明については、公式・大手メディア相当の裏取りでは、OpenAI公式がその証明、64エージェント、Lean検証済みを明確に確認した情報は見当たりません。したがって、CDC突破は現時点では“コミュニティで騒がれている未確認主張”として扱う必要があります。

今回の面白さは、CDCそのものではなく、その発表に触発された別の研究者が、凸最適化の具体的な未解決ギャップにGPT-5.6 Sol Proを使い、Leanで検証された証明が得られたと投稿している点です。Reddit上の投稿者は、UC Berkeley IEORの助教で応用数学PhDだと自己紹介し、プレプリント、Lean証明コード、完全なプロンプトをGitHubで公開していると説明しています。本人も「まだ査読されていない」と明言しているため、これは数学界の確定成果ではありません。しかし、話題の重心はすでに“AIがすごい証明文を書いたらしい”から、“形式検証器が通る形にまで落ちたのか”へ移っています。

【技術的ディープダイブ】
Reddit投稿で主張されている技術的コアは、GPT-5.6 Sol Proが148分の単一セッションで、1996年以来残っていた凸最適化のoracle-complexity gapを閉じる証明の主論証を与えた、というものです。対象プレプリントのタイトルは「Closing the Oracle-Complexity Gap in Derivative-Free Convex Optimization: A Near-Quadratic Lower Bound from Exact Function Values」。ざっくり言えば、勾配を直接使わず、関数値だけを問い合わせるderivative-free convex optimizationで、どれだけの問い合わせが本質的に必要なのか、という下限証明の話です。

投稿者によると、プロンプトは約10ページで、OpenAIのCDC証明発表で使われたprompting methodologyを参考にしたものです。さらに、GPT-5.4やGPT-5.5ではうまくいかなかったが、5.6 Sol Proでは一発で解けた、と説明されています。ここで重要なのは、単なるチャット回答ではなく、Leanで形式検証されたとされる点です。Leanは証明支援系で、人間が読んで“もっともらしい”では済ませず、定理、仮定、補題、型、推論ステップを機械的にチェックします。LLM数学のボトルネックだった幻覚的な証明文を、形式言語のコンパイル対象に変換するパイプラインが見えてきたことが、ギーク的には本丸です。

ただし、ファクトチェック上の線引きは厳密に必要です。公式・学術ソース側で確認できる強い事実としては、別件のSabidussi’s Compatibility Conjecture関連で、GPT 5.6 Proによる証明がLeanで形式化され、論文内でGPT 5.6 Solが執筆補助として記されていることがあります。一方、今回の凸最適化ギャップについては、提供情報の範囲ではReddit投稿と公開リポジトリ中心の未査読主張です。したがって、“Lean検証済みの成果として投稿された”とは言えても、“数学コミュニティに確定受理された”とはまだ言えません。

【コミュニティの生々しい熱量と議論】
Redditの反応で一番刺さっているのは、Lean検証があることで懐疑の対象が変わる、という点です。トップコメントでは「The Lean verification is what separates this from every other ‘model proved X’ thread」と評され、148分の会話ログ全体を信じる必要はなく、形式化されたstatementが本当に元の主張と一致しているかを確認すればよい、という見方が出ています。これはかなり重要です。AI数学の議論はこれまで、証明の各行が本当に正しいのか、人間が読むには長すぎるのではないか、という泥沼に入りがちでした。Leanが通るなら、議論は“証明文が美しいか”ではなく“形式化された定理が本当に欲しかった定理か”へ移ります。

一方で、当然ながら懐疑もあります。「プロンプトを見ていないが、インターネット検索をしたのではないか。既存解がどこかにあったのではないか」という声が出ています。これは妥当な疑問です。LLMが未知の定理を発見したのか、既存文献の断片を再構成したのか、あるいは人間研究者の10ページプロンプトが本質的な研究貢献だったのかは、プレプリント、Leanコード、プロンプト、関連文献の照合が必要です。

さらに皮肉っぽいコメントとして、博士課程の目的が“科学を進めること”から“フロンティアモデルに科学を進めさせるための専門的プロンプトを書けるようになること”へ変わっていくのではないか、という反応もありました。ここに現場のざわつきがあります。研究者がAIの補助輪を使う話ではなく、研究者が問題設定、文脈圧縮、検証境界、形式化確認を担当し、モデルが探索空間を掘るという分業になり始めている。

【今後の展望とエコシステムへの影響】
もしこの流れが本物なら、オワコンになるのは“LLMが自然言語で証明をそれっぽく書きました”というニュース形式です。今後の評価軸は、査読、形式検証、再現可能なプロンプト、公開リポジトリ、定理文の一致確認へ移ります。特に数学・理論CSでは、LLM単体の賢さより、Lean、Coq、Isabelleのような証明支援系と、探索エージェント、文献検索、反例探索、型エラー修正ループを組み合わせた研究パイプラインが主戦場になります。

パラダイムシフトの芯は、AIが“研究者の横で草稿を書く助手”から、“形式検証パイプライン込みで候補証明を生成する発見装置”として見られ始めたことです。ただし、ここで熱狂しすぎると危険です。Leanが保証するのは、形式化された命題から形式化された結論への推論であって、その命題が元の数学的主張を完全に表しているか、仮定が妥当か、重要性がどれほどかまでは保証しません。つまり次のボトルネックは、証明生成から“仕様化”へ移ります。

今回の凸最適化の件は、公式確定ニュースではなく、未査読のコミュニティ発ブレークスルー候補です。しかし、ギーク的な注目点は十分にあります。148分、10ページプロンプト、1996年以来のギャップ、derivative-free convex optimization、Lean検証。これらのキーワードが同じ場所に並んだ時点で、LLM研究の見方は少し変わります。今後は“AIが証明したか”ではなく、“AIが出した証明を、どの形式システムで、どの定理として、誰がどこまで検証したか”がニュースの最低ラインになっていくはずです。