Multi-agent teams for math and software

Google said it has expanded its Antigravity multi-agent system, which uses teams of specialized agents powered by its Gemini models. The company's Teamwork framework relies on agents that independently explore solutions, test approaches and verify results with computational tools. The aim is to reduce errors that can arise when a single model generates a long chain of reasoning.

Notable results

  • Weil conjectures: To formalize results originally proved by Pierre Deligne in 1974, Google's Teamwork-LEAP system produced approximately 1.8 million lines of Lean code across 28,800 subagent invocations.
  • Navier-Stokes: The system reproduced a formalization of a recent proof concerning finite-time blowup in the three-dimensional Navier-Stokes equations, a question open for about 90 years.
  • Courtade–Kumar conjecture: Researchers from Google and academic institutions developed a proof in full generality for the 2013 information theory problem, formalized in Lean 4.

Chemistry and software

Google also applied the approach to molecular chemistry. A team of 30 specialized agents working with a physics-informed simulator identified molecular structures from nuclear magnetic resonance (NMR) data with 95% top-one and 100% top-three accuracy on complex benchmark molecules.

On the software side, agents rewrote the company's libgav1 AV1 video decoder from C++ into approximately 170,000 lines of Rust, achieving exact output parity across a broad test suite. The initial rewrite ran about four times slower; after agents were given profiling tools and tasked with improving performance, the Rust version became 20% to 30% faster than the original C++ implementation on x86_64 and ARM processors. In a separate project, a two-week campaign moved the remaining C++ code in the Zircon microkernel into approximately 800,000 lines of memory-safe Rust, passing kernel unit tests and booting on ARM64 hardware.

Infrastructure and access

Google reported that its agentic scheduling workflow reduced TPU workload preemption by 24% on some hardware types while maintaining service-level objectives and cluster utilization. The company made Teamwork and its iterative coding workflow /boost available through Antigravity. Applications also opened for 10,000 academic researchers to receive six months of free access to its highest usage tier. Google said additional specialized workflows, including formal proof tools, will be made available in the future.