Google、Antigravityの/teamworkで5,000万行のLean 4証明を報告

Google Researchは2026年11月13日、Antigravityのマルチエージェントシステム「/teamwork」を使い、Courtade–Kumar予想を証明して5,000万行のLean 4コードで形式化したなどの研究成果を発表しました。あわせて、これらのツールをAntigravityで外部提供すると発表しました。執筆者はGoogle Fellow兼Google Research副社長のVahab Mirrokni氏です。

Geminiは、Google DeepMindが開発するマルチモーダル対応のAIモデルのファミリーです。

/teamworkの設計

Googleは、現在の言語モデルの2つの限界に対処するために/teamworkを設計したと説明しています。

• 生成の不確実性: 並列探索と専用の反証器(Lean 4の証明チェッカー、変更していないソフトウェアテストスイート、実行シミュレーター、ウェブ検索、ハードウェアカウンターなど)を組み合わせ、どの候補解が正しいかを自動で検証します。
• 長期タスクでの文脈喪失: コンテキストを分割し、各エージェントには担当ステップに必要なファイルとツールだけを渡します。コーディネーターは新しい後続エージェントへタスクを引き継ぎ、批評役・監査役は元の生成者の推論を持たないクリーンなコンテキストで結果を検証します。

ワークフローは宣言的な自然言語パターンとして記述し、ユーザーのプロンプトを最適なパターンへ動的にルーティングします。パターンには分散コーディング、反復的な問題解決(過去の実行から改良した逐次的なsolve-and-verifyループを単体化した/boost)、Long Proof、文書レビューなどがあります。研究にはGemini 4 Argon、Gemini 4 Carbon、Gemini 4 Hydrogenを使用しています。

主な成果と数値

対象	内容
Courtade–Kumar予想(2013年)	Google、CUHK、USC、CMUの研究者がLong Proofパターンで完全に証明。CUHKチームが14変数の最適化問題に帰着し、Geminiが解析的上界や区間演算の証明書の大半を作成。Lean 4で5,000万行
Weil予想	/teamwork-LEAPが完全自律で形式化。約180万行のLean、サブエージェント呼び出し28,800回
Hilbertの第10問題(一般の整数環)	初の形式化。91万9,000行超のLean
3D Navier–Stokes方程式の有限時間爆発	最近の証明の形式化を独立に再現
3D Bochner–Riesz予想	初の形式化。公開済みの非形式証明のギャップを発見・修正

Courtade–Kumar予想では、Geminiが釣り合い関数から非釣り合い関数への拡張を人手なしで行いました。ほかにも、適応的データ解析で2014年からのギャップを閉じるサンプル数上界(Lean検証済み)、STOC 2024の主要な未解決問題を解く組合せ的ブール行列積の決定的アルゴリズム、GMPとビット単位で10億ビットまで一致する新しいO(n log n)整数乗算のC実装、Tarjanの1985年のDeque予想の進展などを挙げています。

Deep Reviewの利用結果

STOC 2027に向けて、全投稿の3分の1超にあたる578件の著者がDeep Reviewによる草稿へのフィードバックを受けました。進行中の著者調査(N=70)の結果は次のとおりです。

項目	割合
フィードバックが「ほぼ事実に即している」または「ほぼ完全に事実に即している」	90%
再び使う	90%
実質的な証明上のバグや数学的に重要な誤字を検出	30%超
修正に1時間超かかる技術的ギャップを検出	14%

提供条件と使い方

• /teamworkは/boostなどのエージェントと並んでAntigravityで利用できます。
• Long Proofや文書レビューなどのパターンは現在Antigravityで利用でき、Deep Reviewは/teamworkの文書レビュー・パターンとして提供されます。
• Deep Reviewはユーザーあたり週2回まで無料で呼び出せます。
• Googleは今後数週間で、全機能を外部ユーザー向けにAntigravityで順次提供する予定です。