Google 推出的 Antigravity /teamwork 讓多個 Gemini 4 代理人分工合作，把研究與工程任務拆成可驗證的小步驟。Google 研究院在 11 月 13 日公布成果：團隊用它證明了 2013 年提出的 Courtade–Kumar 猜想，並自動完成韋伊猜想約 180 萬行的 Lean 形式化，現在 Antigravity 使用者已經可以直接使用，也開放 1 萬名學術研究者申請六個月免費最高用量方案。
/teamwork 是什麼？讓一群代理人互相查核，而不是單一模型碰運氣
/teamwork 是 Antigravity 平台上的多代理人系統，底層使用 Gemini 4 的 Argon、Carbon 與 Hydrogen 三款模型。Google 指出它要解決兩個老問題：單次嘗試的結果不穩定，以及任務拉長到數天後上下文會流失。對應的做法是讓多個代理人平行探索，再交給「證偽器」判斷哪些解答真的成立，這些證偽器包括 Lean 4 證明檢查器、測試套件、模擬器、網路搜尋與硬體計數器。
每個代理人只拿到完成工作所需的檔案與工具，協調者會把進度交給全新的接班代理人，批評者與稽核者則在乾淨的上下文中重新檢查結果。使用者送出提示後，系統會自動挑選合適的工作流程，例如長證明、文件審查 Deep Review、迭代式寫程式的 /boost，或是 DuoDiscover。
數學與理論電腦科學：從猜想證明到大規模形式化
Google 公布的數學成果是這次最吸睛的部分。在與香港中文大學、南加州大學與卡內基美隆大學研究者合作下，團隊宣稱完整證明了 2013 年提出的 Courtade–Kumar 猜想，證明以 Lean 4 形式化後規模約 5,000 萬行。另外，團隊也宣稱補上了 2014 年以來適應性資料分析的樣本界限缺口，並解決了 STOC 2024 留下的布林矩陣乘法主要開放問題，得到確定性演算法。
在形式化驗證方面，搭配 Argon 的 LEAP 框架自主完成韋伊猜想約 180 萬行的 Lean 程式碼，期間呼叫子代理人 28,800 次；Interesting Engineering 指出，這些結果原本是 Pierre Deligne 在 1974 年證明的。希爾伯特第十問題針對一般整數環的近期證明，則產生超過 91.9 萬行 Lean 程式碼。Google 還表示重現了三維 Navier–Stokes 方程式有限時間爆破的端到端形式化，並首度完成 Birkhoff 猜想與三維 Bochner–Riesz 猜想的形式化，其中後者還找出了近期非形式化證明中的一處缺口。
目前這些成果都是 Google 與合作研究者自行公布，Interesting Engineering 的報導也沒有引述外部數學家的驗證；Lean 形式化本身可由證明檢查器核對，但猜想證明在學界的接受度，還要看後續論文與同儕檢視。
Deep Review：STOC 2027 超過三分之一投稿選擇讓 AI 先審稿
對一般研究者來說，更貼近日常的是 Deep Review。Google 表示，STOC 2027 共有 578 份投稿選擇使用它，占總投稿數超過三分之一。在 70 位回覆問卷的作者中，90% 認為回饋大致或幾乎完全符合事實，也有 90% 願意再次使用；超過 30% 表示它抓到了證明錯誤或重大筆誤，14% 表示發現了需要一小時以上才能修補的技術缺口。
化學、系統與程式工程：從 NMR 分子辨識到 Rust 改寫
在化學領域，30 個代理人搭配物理資訊光譜模擬器，對複雜 NMR 基準分子達到 95% 的 top-1 與 100% 的 top-3 完全吻合，Google 稱幾乎是單一代理人表現的兩倍。
工程面的數字也很具體：連通元件演算法擴展到 1 兆條邊的圖，吞吐量提升 60 到 90 倍；客製 GNN TPU 核心讓高頻寬記憶體用量最多降低 185 倍；9×9 圍棋引擎在不到八天內提升約 2,600 Elo。Google 也提到團隊用約 80 萬行安全 Rust 擴充 Zircon 微核心移植，並把 17 萬行的 libgav1 AV1 解碼器改寫成 Rust，輸出與原版逐位元一致，最終比原本的 C++ 與組合語言版本快 20% 到 30%。在 Google 內部，Borg 排程的代理人工作流程讓部分硬體上的 TPU 工作負載搶占減少 24%，同時維持服務水準目標。
現在能用什麼？Antigravity 已上線，研究者可申請六個月免費
搭載 Gemini 4 的 /teamwork、/boost 與 Deep Review 現在已在 Antigravity 開放。Google 同時開放 1 萬名學術研究者申請六個月最高用量方案的免費使用，需要透過申請表單。形式化證明與程式碼重寫等專用工作流程，Google 表示將陸續推出，並會在 Antigravity 部落格提供教學。
對開發者與研究團隊而言，這次發表的重點不只是個別猜想，而是「平行嘗試加上可自動驗證的證偽器」這種做法能否成為長時程任務的標準流程。能被 Lean 或測試套件自動檢驗的工作，最容易受益；缺乏明確驗證手段的任務，是否同樣有效，Google 這次沒有提供數據。
更多AI相關報導
- Google Antigravity 推出 /teamwork：多個 Gemini 4 代理人合作，證明 Courtade–Kumar 猜想並完成韋伊猜想形式化
- OpenAI 推出 ChatGPT Wallet，dots 代理人能替 Pro 用戶刷卡購物，每筆都要 Face ID 確認
- Gemini 4 Hydrogen 發表：對標 Claude Sonnet 5.5，API 輸入每百萬 token 1.5 美元
- Claude for Manufacturing 登場：直接幫工廠擬報價、查品檢失敗原因、排序機台故障成因
- Google 推出 Gemini Decisions API，只做選擇題不寫字，輸入每百萬 token 0.1 美元、輸出免費
