Google 展示 Antigravity /teamwork 多智能体协作成果并开放给研究者使用

Over the past several weeks, teams across Google and academic partner institutions have tackled open problems in math, science, and complex systems engineering that had remained open for years. Using Gemini 4 Argon, Gemini 4 Carbon, Gemini 4 Hydrogen and multi-agent workflows such as Antigravity’s /teamwork (building on various Gemini models), these collaborations have produced new innovations across information theory, formal verifications, molecular structure discoveries, and kernel optimization, along with several production infrastructure gains at Google. We are making these agentic tools available in Antigravity’s /teamwork (alongside /boost and other agents) so that researchers and developers can apply them to their own work.

Frontier research and systems engineering require navigating vast literature, building custom computational pipelines, testing against physical measurements, and verifying every step. Progress comes from an interactive discovery loop where researchers frame questions and define the theoretical or physical constraints, while long-horizon agents write custom solvers, explore large search spaces, test candidate designs, and check long chains of logic.

Scaling long-horizon reasoning

Two limits of current language models motivate /teamwork's design. First, model generation can be unpredictable, leaving a gap between a single attempt and finding the correct answer. The system bridges this gap by pairing parallel exploration with dedicated falsifiers (e.g., the Lean 4 proof checker, unmodified software test suites, execution simulators, web search, or hardware counters) to automatically verify which candidate solutions work.

Second, AI models often lose track of details over multi-day tasks because attention disperses across growing context windows. To prevent this, /teamwork partitions context by construction: each specialized agent receives only the exact files and tools it needs for a specific step. Coordinators hand off tasks to fresh successors, while critics and auditors challenge and verify results from clean contexts without the original producer's reasoning.

Teamwork expresses these workflows as declarative self-improving natural-language patterns and dynamically routes each user prompt to the pattern best suited to the task. These patterns range from distributed coding and iterative problem-solving (packaged standalone as /boost, a sequential solve-and-verify loop refined from prior trajectories) to specialized research workflows like long proof and document review, all of which are available in Antigravity today. This allows teams to design custom specifications from past run transcripts routing across different harness patterns and dynamically improving agentic harness. While many of these features are available in Antigravity, we will provide more updates in the coming weeks providing all the features to our external users on Antigravity. Following our previous posts on Antigravity /teamwork, we provide new results to open challenges empowered by new variants of /teamwork and Gemini 4 models.

Mathematics and theoretical computer science

Across mathematics and theoretical computer science, researchers paired with Gemini 4 and /teamwork harnesses to collaborate on large-scale proofs and generate complete algorithms and proofs directly from open problem statements. We present several examples.

Proving and verifying the Courtade–Kumar conjecture

Researchers from Google, CUHK, USC, and CMU used /teamwork's Long Proof pattern (implementing Stellar Colosseum in Antigravity) to prove information theory's 2013 Courtade–Kumar conjecture in full generality. The result confirms that when a random bit string passes through a noisy channel, no compression of the input to a single bit preserves more information than a "dictator function", which just copies a single input bit. Gemini first found counterexamples to a generalized conjecture from the CUHK team's earlier paper. The CUHK team then proposed a new candidate function that reduced the conjecture to a 14-variable optimization problem, along with a key analytical lower bound. Gemini 4 Argon and earlier Gemini models then partitioned the parameter space and developed most of the new analytical bounds and interval-arithmetic certificates. They also extended the proof from balanced to unbalanced functions without human input. The team formalized the entire proof in Lean 4, producing 50 million lines of code.

Resolving open questions in optimization, statistics, quantum computing, and algorithms

Researchers also posed open problems directly to Gemini 4 and to multi-agent harnesses such as Stellar Colosseum and /teamwork, receiving end-to-end algorithms and proofs (often with Lean 4 formalizations) that the authors verified, simplified, and edited for publication. In adaptive data analysis, a multi-agent harness running on Gemini 4 Argon independently proved and Lean-verified near-optimal sample bounds for statistical queries chosen adaptively from earlier answers, closing a gap open since 2014. These bounds yield the first nearly space-optimal algorithm for data streams with both insertions and deletions that stays accurate against adaptive adversaries. In quantum computing, a new construction settled a 2014 open question by finding the first n-bit Boolean functions needing strictly more than n/2 quantum queries at constant error, while pinning down the exact query overhead across symmetric functions.

Several results break long standing barriers in processing and compressing large matrices and graphs. For fifty years until STOC 2024, combinatorial algorithms for Boolean matrix multiplication and triangle detection (avoiding the algebraic cancellations of fast matrix multiplication) saved only logarithmic factors over cubic time. A new deterministic algorithm resolves STOC 2024's main open question, achieving its target speedup over cubic time. In high-dimensional geometry, a new lower bound resolves an open problem on sparse networks, proving that approximating all pairwise distances among n points within any constant factor can require polynomially more than n edges, even with extra Steiner points and arbitrarily many hops. In randomized linear algebra, stacked sparse sketches resolve a 2025 open question by breaking the classical sparsity barrier for compressing a matrix to linear dimension without collapsing any direction of an r-dimensional subspace, needing only √log r nonzeros per row (quadratically fewer than the log r required to preserve all lengths) and nearly matching a new lower bound. For weighted graphs under dynamic edge-weight insertions and deletions, Stellar Colosseum resolved an open question left by FOCS 2022, developing the first single-pass streaming algorithm for cut sparsification that achieves near-optimal memory, update time, and reconstruction time simultaneously.

Our results also span optimization, arithmetic, data structures, and statistics. In optimization, resolving an open question on online inverse linear optimization (inferring an expert's hidden objective from decisions over time), the approach gave a deterministic algorithm achieving optimal regret while cutting runtime from exponential in the dimension to polynomial time. For n-bit integer multiplication, multi-agent campaigns simplified the theoretical Turing-machine bound below n log n, while a separate effort gave a new O(n log n) algorithm on a single two-dimensional grid whose C implementation matches the GNU Multiple Precision Arithmetic Library (GMP) bit-for-bit up to a billion bits. In data structures, another result made significant progress on Tarjan's 1985 Deque Conjecture (whether self-adjusting splay trees handle insertions and deletions at both ends in constant amortized time), proving a new upper bound on the per-operation overhead that simultaneously beats every finitely iterated inverse-Ackermann function, verified in Lean 4. Finally, in high-dimensional statistics, the approach proved that approximate leave-one-out cross-validation, which avoids refitting the model from scratch, remains accurate for non-smooth sparse penalties like elastic net.

Scaling formal verification and manuscript review

Checking a computer-assisted manuscript by hand places a heavy burden on peer reviewers, and subtle flaws can hide inside long calculations. Formalizing mathematics in Lean 4 turns a proof into code that a computer kernel checks line by line. Once human mathematicians confirm that the formal theorem statement matches the original problem, the proof only compiles if every logical step holds.

Many of the deepest open problems in mathematics govern how physical waves propagate, how dynamical systems evolve, and whether polynomial equations have integer solutions. Working directly from informal proofs, our multi-agent framework, LEAP, developed with colleagues in Google Cloud AI and paired with Argon, has made progress in these core areas.

Notably, /teamwork-LEAP fully autonomously produced an end-to-end, machine-checked formalization of the Weil conjectures, the landmark results on counting solutions of polynomial equations over finite fields that culminated in Pierre Deligne's 1974 proof. This formalization spans about 1.8 million lines of Lean, produced across 28,800 subagent invocations. The system also synthesized over 919,000 lines of Lean to produce the first formalization of a recent proof of Hilbert's tenth problem over general rings of integers. It also independently reproduces an end-to-end formalization of a recent proof of finite-time blowup for the 3D Navier–Stokes equations with smooth forcing, part of one of the seven Millennium Prize Problems and open for about 90 years.

Beyond these, it also generated the first formalization of the Birkhoff conjecture, a dynamical-systems problem open since 1927. Moreover, it formalized for the first time the 3D Bochner–Riesz conjecture, a central problem in harmonic analysis open for more than 50 years, finding and fixing a gap in a recently released informal proof along the way. Additional machine-checked breakthroughs include resolving the C¹ regularity of infinity-harmonic functions in three and higher dimensions (an open question for about 20 years), formalizing Killip and Vişan's theorem that the KdV water-wave equation is well-posed in H⁻¹ and verifying a UCLA group's informal proofs of the 40-year-old Jamison Caterpillar Conjecture, the Ağırseven-Ollis conjecture, and an improved upper bound on Erdős Problem #1063.

Finally, we provided Deep Review for authors of another CS conference: ahead of STOC 2027, authors of 578 submissions (over a third of all submissions) opted in to receive Deep Review feedback on their drafts. In an ongoing author survey (N = 70), 90% of respondents rated the feedback mostly or almost all factual and 90% said they would use the tool again. Over 30% said Deep Review caught substantive proof bugs or mathematically significant typos, and 14% said it found technical gaps that took more than an hour to fix. Surveyed authors shared that “Tools of this kind can help produce cleaner and more precise research, faster” and that DeepReview provides peace of mind on scientific discovery”. We provide users two weekly calls to Deep Review for free. Deep Review is also implemented as /teamwork's document review pattern and available in Antigravity. Read more about DeepReview in our recent blog post.

Molecular chemistry discovery

Beyond formal proofs, pairing specialized generator agents with independent verifier agents enables discovery workflows in experimental laboratory science.

Determining a molecule’s structure from experimental nuclear magnetic resonance data is one of chemistry’s hardest puzzles. For example, in HIV protease inhibitors, one misplaced bond separates an inactive look-alike from a drug. By organizing 30 specialized agents into a self-correcting loop with /teamwork and a physics-informed spectral simulator, we achieved 95% top-1 exact match and 100% top-3 accuracy on complex benchmark molecules, nearly doubling single-agent performance. Beyond teaching Gemini to reason over structure, this lays the groundwork for ongoing works on 3D protein and complex structures dynamics.

Beyond this example, science problems including applications in nuclear fusion and quantum algorithms reported in the Gemini 4 blog post benefited from /teamwork and the Argon model.

Generating a causal inference benchmark

We also applied a similar multi-round auditing workflow to build empirical benchmarks. Starting from five human-specified acceptance criteria like data anonymization, 29 agents running on Argon over 11.5 hours turned 13 public tables into a 50-task causal inference benchmark. In these tasks, models must determine whether a causal effect can be identified and estimate it against a known answer. After initial checks, separate reviewer and auditor agents caught shortcuts, flagged wording hints, and vetoed hallucinated scripts, turning each into a permanent test. Automating this heavily manual task generation supplies the hard problems needed to help Gemini answer counterfactual "what-if" questions.

Coding and systems engineering

When paired with objective evaluators such as network benchmarks, game engines, unmodified test suites, and hardware timers, /teamwork campaigns can execute multi-day software and hardware engineering projects.

Distributed systems

Using /teamwork and Argon, we built FarArray, a low-latency kernel-bypass Partitioned Global Address Space based on the SNAP microkernel. Applications built on FarArray include lock-free Connected Components, which scale to 1-trillion-edge graphs with 60x to 90x throughput gains and 40x to 180x speedups at 6x lower RAM over TCP key-value stores. Similarly, InstantEmbedding (Personalized PageRank) reduced peak DRAM by up to 14x and runtime by 11x to 27x over accelerated MapReduce implementations. The team also used /teamwork and Argon to create custom TPU kernels for Graph Neural Networks, delivering up to a 185x High Bandwidth Memory reduction and 8x to 15x speedups in forward and backward passes. Further details are available in our recent Antigravity blog post.

Autonomous hill climbing

To test autonomous optimization over long horizons, hill-climbing teams on Argon trained a 9x9 Go engine from scratch starting from a basic AlphaZero implementation. Human researchers set the chip allocation and evaluation setup, while the harness ran autonomous campaigns for faster self-play (achieving a 2,300x speedup) and faster Elo readings, promoting champions strictly via statistical tests on locked records. In under eight days, the engine gained roughly 2,600 Elo, reaching 1,885 Elo, placing it between KataGo at 16 and 32 visits per move.

Memory-safe Rust rewrites, /boost, and TPU kernel optimization

Large code migrations fail when agents stub out dependencies or alter tests to make a broken port pass. A new /teamwork rewrite pattern, soon to be available in Antigravity, solved this by scheduling each module only after its dependencies compile, linking every leaf module against the original, unmodified test suite. Building on the initial 25% port of the Zircon microkernel, a two-week Argon campaign rewrote the remaining C++ code, adding about 800,000 lines of safe Rust that pass all kernel unit tests and boot on arm64 hardware. /teamwork also rewrote libgav1, Google's AV1 video decoder, from C++ into around 170k lines Rust, achieving 100% bit-exact parity across a broad conformance test suite. Initially, the port was around 4x slower than the original C++ code. However, after giving /teamwork access to profiling tools and a mandate to maximize speed on sample video clips, the Rust port became 20-30% faster than the original C++ and hand-optimized assembly code on both x86_64 and ARM.

For day-to-day coding tasks, the Antigravity /boost command packages /teamwork's iterative coding pattern. A long-running /teamwork campaign analyzed past run trajectories and found that tightly coupled code is best handled through sequential implementation and revision stages rather than parallel splits, improving /boost on coding tasks. This is an example of a harness optimizing another harness for token efficiency.

For machine learning systems, full hardware evaluations of custom JAX and Pallas TPU kernels take 7 to 32 minutes, limiting how many candidates prior optimization agents can explore. Using /teamwork's DuoDiscover pattern on Argon, four parallel agents identified performance bottlenecks and constructed fast, 23-second proxy evaluators called yardsticks. These yardsticks produce candidate orderings that are continuously validated against periodic full hardware runs using Kendall's rank correlation. DuoDiscover achieves a 4.09x geometric-mean speedup over reference implementations across 17 JAXBench kernels and a 2.99x geometric-mean speedup across 7 hand-optimized vLLM TPU-Inference Pallas kernels for frontier open-weight models.

Google infrastructure applications

We have also applied /teamwork and /boost to many production infrastructure and hardware modeling problems across Google. Examples include:

• Fleet-wide memory optimization: Building on the initial Argon memory efforts, we analyzed fleet-wide metrics, as well as internal memory saving past successes, and created reusable /teamwork workflows that have identified memory saving opportunities, surpassing our initial savings estimates of 1 PiB. We also deployed the human-in-the-loop Memory Efficiency Monitoring Agent, achieving additional memory savings, using techniques such as struct padding elimination, scalar narrowing, cliff jumping, outlining, and tagged pointers.
• Borg agentic scheduling: Built on /teamwork and /boost, Borg’s agentic workflow for scheduling optimization shipped 2 successful changes, resulting in a 24% reduction in TPU workload preemption on some hardware types, while preserving workload SLOs and cluster utilization.

Opening these tools to the research and developer community

External scientists and developers can use Gemini 4 models with /teamwork and /boost in Antigravity and Deep Review today. We have also opened applications giving 10,000 academic researchers six months of free access to our highest usage tier. Upcoming updates will bring our formal proof pattern and additional specialized workflows into Antigravity. These features will be accompanied by deep-dive tutorials on the Antigravity blog in the coming weeks, ensuring that developers and researchers have the resources needed to generate, inspect, and iteratively refine custom multi-agent teams. We are excited to make our tools (in addition to our models) available for everyone.

Acknowledgements

Antigravity’s /teamwork feature is a result of a Google-wide effort with many contributors and ongoing explorations. Contributions include: Yuan Deng[279eb3], Honghao Lin[279eb3], Jieming Mao[279eb3], Vahab Mirrokni[279eb3], Vishnu Veeramachaneni[279eb3], David Woodruff[279eb3], Song Zuo[279eb3], Shubham Agarwal, Santiago Balseiro, MohammadHossein Bateni, Mohsen Bayati, Garrett Bingham, Guy Blelloch, Douglas Chen, Vincent Cohen-Addad, Piaoyang Cui, Tulsee Doshi, Eric First, Michael Galkin, Elena Gribelyuk, Anupam Gupta, Guru Guruganesh, Mike Heddes, Patrick Heisel, Iman Hosseini, Kevin Hou, Lalit Jain, Adel Javanmard, Rajesh Jayaram, Xiaoen Ju, Po-Nien Kung, Silvio Lattanzi, Samuel Lavoie, Chun-Liang Li, Matthew Li, Yinan Li, Yuchen Li, Yiming Liu, Thang Luong, Brandon Mayer, Simon Meierhans, Swaroop Mishra, Ashish Naik, Sebastian Nowozin, Renato Paes Leme, Nikos Parotsidis, Ali Parviz, Neel Patel, Violet Peng, Bryan Perozzi, Anshul Ramachandran, Shashir Reddy, Lijie Ren, Madhavi Sewak, D Shin, Reza Shokri, Sukhdeep Singh, Samuel Smith, Linfeng Song, Dilara Soylu, Zheng Tan, Sasan Tavakkol, Hadi Tavassol, Yifeng Teng, Tom Wollschläger, Haifeng Xu, Zicheng Xu, Yihao Xue, Amir Yazdanbakhsh, and Goran Žužić. Carla Bromberg and Lauren Fraser for program management, and Francis Duan, Pan-Pan Jiang, Xiyan Shao, Jane Shapiro, Weilun Shi, and Xinyu Ye for their contributions to the project. We also thank support from several leaders Sergey Brin, Demis Hassabis, Koray Kavukcuoglu, Pushmeet Kohli, James Manyika, Yossi Matias, Varun Mohan, and Amin Vahdat.

Several academic collaborators contributing to the research papers: Zijie Chen, Amin Gohari, Chandra Nair (CUHK), Songbin Liu, Arian Maleki, Chen Shang, Hanbo Yang, Wenjin Zhang (Columbia University), Zihan Hao, Qipeng Liu, Jianan Shao (UCSD), Lorenzo Beretta (IBM Cambridge), Simone Bombari (BYU & Flatiron Institute), Mahbod Majid, Margalit Glasgow (MIT), Raphael Arkady Meyer (UC Berkeley, ICSI, & LBNL), Kijun Shin (CMU), Huacheng Yu, Elena Gribelyuk (Princeton University), Xin Lyu (UCB/ ByteDance), Samson Zhou (Texas A&M), Erik Waingarten (UPenn), and Sorrachai Yingchareonthawornchai (ETH-ITS).