7月19日、RuntimeWire.comが「Berkeley researcher used GPT-5.6 to derive a Lean-verified optimization bound」と題した記事を公開した。UCバークレーの研究者がOpenAIの最新モデルGPT-5.6を用いて凸最適化における長年の未解決ギャップを埋める下界を導出し、定理証明支援系Lean 4で形式検証したという事例だ。AIが査読可能な数学的議論を生成できることを具体的に示した事例として注目を集めている。

GPT-5.6が148分かけて証明した凸最適化の下界

UCバークレーで助教を務めるPhillip Kerger氏が、OpenAIのGPT-5.6 Sol Pro（2026年7月時点でのOpenAI最新モデル）を用いて凸最適化の新たな下界を求める中心的な議論を生成し、その結果を定理証明支援系Lean 4で形式検証した。プレプリントは7月14日に提出され（36ページ）、7月15日にKerger氏自身がその経緯を公開した。なお、本論文はまだ査読を経ていない。

対象となるのは確定的ゼロ次凸最適化（zeroth-order convex optimization）だ。アルゴリズムは関数値のみを観測でき、勾配などの追加情報は得られない。シミュレーターや物理実験から結果だけが返ってくるような設定に対応する。

この分野では長年、「最悪ケースでの最適化に必要な関数評価回数」について上界と下界の間に大きなギャップが存在していた。1996年に示された上界は次元$d$に対して準二乗のオーダーを要求するものだったが、当時知られていた下界は線形オーダー（次元に比例する程度）にとどまっており、両者の間には対数因子を除いた二乗分のギャップがあった。

Kerger氏の論文はこのギャップを対数因子を除いてほぼ解消した。準二乗の下界を確立することで、確定的な関数値のみを用いる手法が従来知られていた線形下界を一般に達成できないことが確実に示される。上界と下界の双方が準二乗オーダーで対応し、残るのは対数因子だけとなった。

なお、これは「ある固定された回数の評価が厳密に必要」という意味ではなく、下界と上界がともに準二乗的な水準で収束したという意味である。数式を用いた詳細な定式化は元記事および論文プレプリントを参照されたい。

プロンプトには「1年分の研究」が詰まっていた

Kerger氏はジョンズ・ホプキンス大学で応用数学のPhDを取得し、最適化・アルゴリズム・計算複雑性を専攻。NASAの量子人工知能研究所（QuAIL）で分散量子アルゴリズムの研究にも携わった経歴を持つ。凸最適化や混合整数最適化の情報複雑性に関する先行研究も持ち、今回の問題の定式化を正確に行える立場にあった。

GPT-5.6に投じた最初のプロンプトは約10ページ。OpenAIが「Cycle Double Cover Conjecture」の研究で公開したプロンプトの構造を参考に設計されており、数学的な設定の記述、有望なアプローチのリスト、失敗した試みからのアイデア、そして「解として認めない結果」の定義が含まれていた。

Kerger氏は同じ問題についてGPT-5.4やGPT-5.5でも試みたが失敗。最終結果に現れたものと同系統のハード関数族に向けてモデルを誘導しても、証明を完成させることができなかった。

GPT-5.6による成功した証明探索セッションは148分間で完了した。ただしこの数字は「最終的な中断なしのセッション」の時間であり、問題を定義し、プロンプトを磨くために費やした約1年分の研究時間は含まれない。元の会話では、より厳しい精度設定での主要な構成と証明の議論が生成された。後続セッションで、論文に記載された精度設定に精緻化されている。

Lean 4による形式検証が「信頼性の基盤」になる

Kerger氏は論文と並行して**Lean 4リポジトリ**を公開した。Leanは関数型プログラミング言語と定理証明支援系を兼ねたシステムであり、数学的命題に対して証明が成立しているかどうかをカーネルが機械的にチェックする。リポジトリには確定的下界定理の形式化が含まれる。

これにより、もっともらしく見えて実は誤りのある推論ステップが混入するリスクを大幅に減らせる。ただしLeanの検証範囲は確定的下界定理に限定されており、既知の上界と混合整数最適化への結果の移植は形式化の外にある。

Kerger氏は論文・プロンプト全文・モデルとのやりとりのログ・ソースコード・証明マップ・ビルド手順・形式証明確認用の比較設定をすべて公開している。これは「謝辞にAIと記載するだけ」の論文よりはるかに高い開示水準だ。

人間・LLM・定理証明系の分業

今回の事例が示す分業の構造は明確だ。

• Kerger氏：未解決問題の定式化、失敗した試みの蓄積、探索指示の構築、結果の監査
• GPT-5.6：148分の証明探索、下界を完成させる構成の発見
• Lean：符号化された下界証明が正しく成立していることの機械的検証

フロンティアモデルが専門家によって丁寧に設計されたプロンプトと組み合わさることで、査読可能な数学的議論を生成できることを示す事例として、AI支援数学研究の分野で参照される可能性がある。

詳細はBerkeley researcher used GPT-5.6 to derive a Lean-verified optimization boundを参照していただきたい。