Google publishes results from tackling open problems with multiple AI agents
Google on Nov. 13 (Nov. 14 Japan time) published on the Google Research blog results from tackling unsolved challenges in mathematics, chemistry and software development using "/teamwork," a feature of its development tool "Antigravity," and related tools. /teamwork is a feature that has multiple AI agents (systems in which AI carries out work on its own) with divided roles work together. According to the official blog, researchers at Google and partner universities spent the past several weeks using "Gemini 4 Argon," "Gemini 4 Carbon," "Gemini 4 Hydrogen," /teamwork and other tools to work on problems that had gone unsolved for years. All of the results came from collaboration with human experts, and Google says it is making these tools available externally.
Vahab Mirrokni, the author of the official blog post, whose byline reads "Google Fellow and VP, Google Research," announced the results on X early on Nov. 14 Japan time. In the post, he described /teamwork and "DeepReview," which checks research manuscripts, as "powered by Gemini 4 models," and said more than 10 open problems in mathematics and theoretical computer science had been solved. The count does not appear in the official blog.
Check out our recent results solving open challenges across math/science and engineering with /teamwork and Gemini 4 models : https://t.co/in8niq88d4 Details: Following our recent updates on Antigravity’s /teamwork, we’ve been hard at work solving open challenges with our multiagent workflows (/teamwork and DeepReview powered by Gemini 4 models) and pushing these tools externally for everyone to use. Through close collaboration with academic partners, we are evolving these tools into true research and engineering partners designed to tackle open problems. We just posted on the Google Research blog providing a few recent examples : * Math Open Problems & Formal Verification: Reporting 10+ open math and CS theory problems solved including 50M-line Lean 4 proof of Courtade–Kumar conjecture plus open problems in quantum query complexity, Tarjan's Deque Conjecture. Also autonomous Lean formalizations of the Weil (1.8M lines), Birkhoff, and 3D Bochner–Riesz conjectures via Teamwork-LEAP, plus updates on Deep Review for STOC’27. * Chemistry & Discovery: 95% top-1 exact match on NMR molecular structure elucidation (nearly 2× single-agent). Also empowering Nuclear Fusion and Quantum algorithm results as well autonomously generating a CausalAnalyst Benchmark. * Systems, TPU Kernel, & Infra: * Clustering 1-Trillion-edge graphs on FarArray and RDMA (up to 180× faster), * 800K-line Zircon & 170K-line libgav1 safe Rust rewrites (20–30% faster than C++/ASM), * 4.09× JAXBench TPU kernel speedups with DuoDiscover, * surpassing 1 PiB fleet memory savings, and 24% fewer Borg TPU preemptions. Best of all, these tools are available externally in Antigravity. Previously, when we developed agents for coding and math competitions and later for science acceleration, we relied on internal models and agentic tools; now, I am happy we can share these tools with everyone—with Hydrogen models available to all, and Carbon and Argon models for Enterprise and Ultra/Paid users. We’re also opening applications for 10,000 academic researchers to get 6 months of free access to our highest usage tier for Antigravity. We also provide two free weekly DeepReview calls for all. This is a collaboration across many at Google (in Gemini, Antigravity, Research, Cloud); Congratulations to the whole team! We will post more details in Antigravity blog post. Apply for the academic researcher access program: https://t.co/BfuStASb4W, and Try DeepReview: https://t.co/r26ksY3COc Read the full blog here : https://t.co/in8niq88d4 #AntiGravity #Gemini4 #teamwork #AI4Math #AI4Systems #AI4Coding
Demis Hassabis, a co-founder of Google DeepMind, reposted the post early on Nov. 15 Japan time. He did not add any comment of his own.
According to Google, /teamwork is designed to make up for the fact that a model's answers are not the same each time and that it tends to lose track of details over work lasting several days. Multiple agents search for answers in parallel and automatically check which answers are correct using the Lean 4 proof checker, existing test suites and other tools. Each agent receives only the files and tools needed for its task, and critic and auditor agents check the results without seeing the reasoning of the agent that produced them.
Information theory conjecture proved and verified in 50 million lines of Lean 4
In mathematics, Google cited a proof of information theory's "Courtade–Kumar conjecture," posed in 2013. The conjecture holds that when a random bit string passes through a noisy channel, no way of compressing the input to a single bit preserves more information than simply copying one bit of the input. Researchers from Google, the Chinese University of Hong Kong (CUHK), the University of Southern California (USC) and Carnegie Mellon University (CMU) used /teamwork's procedure for long proofs to prove it in full generality.
According to the official blog, Gemini first found counterexamples to a generalized conjecture in an earlier paper by the CUHK researchers. The CUHK researchers then proposed a new candidate function and narrowed the problem to a 14-variable optimization problem. Gemini 4 Argon and earlier Gemini models then partitioned the range to be examined and produced most of the new analytical bounds and the interval-arithmetic certificates. The research team formalized the entire proof in Lean 4, producing 50 million lines of code.
In addition, on an adaptive data analysis problem open since 2014, multiple agents running on Gemini 4 Argon independently proved near-optimal sample bounds and verified them in Lean. In quantum computing, a new construction answered an open question from 2014. On "Tarjan's Deque Conjecture," posed in 1985, the work did not resolve the conjecture itself but showed a new upper bound that makes significant progress, verified in Lean 4. Google said researchers posed problem statements to Gemini 4 and to multi-agent systems, and the authors verified, simplified and edited the resulting proofs for publication.
Weil conjectures formalized autonomously in about 1.8 million lines; 578 STOC submissions checked
Google also reported results in formalization (rewriting a mathematical proof into code that a computer can check line by line). It said it combined "LEAP," a multi-agent system developed with Google Cloud AI, with /teamwork and used it with Argon. The system formalized the "Weil conjectures" on the number of solutions of polynomial equations over finite fields (whose proof Deligne completed in 1974) fully autonomously. The formalization runs about 1.8 million lines of Lean and involved 28,800 calls to subagents.
It produced the first formalization of the "Birkhoff conjecture," a dynamical-systems problem described as open since 1927, and also formalized for the first time the "3D Bochner–Riesz conjecture," a problem in harmonic analysis open for more than 50 years. For the Bochner–Riesz conjecture, Google said the system found and fixed a gap in a recently released proof.
DeepReview, which checks research manuscripts, was offered to authors submitting to "STOC 2027," an international computer science conference. Authors of 578 submissions, more than a third of all submissions, chose to receive feedback on their drafts. In an ongoing author survey (70 respondents), 90% said the feedback was mostly or almost all factual and 90% said they would use the tool again. More than 30% said it caught errors in proofs or mathematically significant typos, and 14% said it found technical gaps that took more than an hour to fix.
In chemistry, 95% match with the correct answer in determining molecular structures
In chemistry, the tools were used to determine molecular structures from nuclear magnetic resonance (NMR) experimental data. Thirty agents were combined with a physics-based simulator that reproduces spectra into a system in which they correct each other's errors. On a benchmark of complex molecules, the top candidate exactly matched the correct answer 95% of the time, and the correct answer was among the top three candidates 100% of the time. Google said this nearly doubles the performance of a single agent, but the official blog does not give the single-agent figure.
The official blog says /teamwork and Argon also helped with results in nuclear fusion and quantum algorithms reported in the Gemini 4 blog post. In building a causal inference benchmark, 29 agents running on Argon created 50 tasks from 13 public data tables in 11.5 hours. Mirrokni's post calls this the "CausalAnalyst Benchmark."
In software rewrites, Rust version runs 20-30% faster than the original C++
In systems development, /teamwork was combined with measurement tools and tests and assigned development work lasting several days. Google's video decoder "libgav1" was rewritten from C++ into about 170,000 lines of Rust, and its output matched the original bit for bit across a broad conformance test suite. Right after the rewrite it was about four times slower than the original C++, but after it was given profiling tools and told to maximize speed, it became 20-30% faster than the original C++ and hand-optimized assembly on both x86_64 and ARM.
For the "Zircon" operating system kernel, following an earlier port of 25%, a two-week effort using Argon rewrote the remaining C++ code, adding about 800,000 lines of safe Rust. Google said it passes all kernel unit tests and boots on arm64 hardware. However, this rewrite procedure is at the stage of being "soon to be available" in Antigravity.
In data processing, Google built "FarArray," a low-latency system for sharing memory. Computations built on it scale to graphs with 1 trillion edges and, compared with key-value stores connected over TCP, achieved 60x to 90x higher throughput and 40x to 180x speedups while using one-sixth the memory. For optimizing programs for TPUs (Google's in-house AI chips), Google used a /teamwork procedure called "DuoDiscover" with Argon. Where a full hardware evaluation takes 7 to 32 minutes, it built substitute evaluations that take 23 seconds to narrow down candidates, and achieved speedups of 4.09x over reference implementations across 17 JAXBench kernels and 2.99x across 7 vLLM TPU kernels (both geometric means).
Google also applied the tools to its internal infrastructure. For memory across its server fleet, it identified savings opportunities exceeding its initial estimate of 1 PiB (pebibyte). In "Borg," its internal system for allocating computing resources, it shipped two changes that reduced TPU workload preemptions by 24% on some hardware types.
| Field | Target | Figures given by Google |
|---|---|---|
| Mathematics | Proof of the Courtade–Kumar conjecture | 50 million lines of Lean 4 |
| Formalization | Weil conjectures | About 1.8 million lines of Lean, 28,800 subagent calls |
| Manuscript review | DeepReview for STOC 2027 | Used for 578 submissions; 90% of survey respondents rated it factual |
| Chemistry | Molecular structure determination by NMR | 95% top-1 exact match, 100% in top 3 |
| Software | Rust rewrite of libgav1 | About 170,000 lines, 20-30% faster than the original C++ and assembly |
| Software | Rust rewrite of Zircon | About 800,000 lines added, passes all unit tests |
| TPU | Kernel optimization with DuoDiscover | 4.09x across 17 JAXBench kernels |
| Internal infrastructure | Allocation changes in Borg | 24% fewer TPU preemptions on some hardware |
10,000 researchers get the top usage tier free for 6 months; DeepReview free twice a week
According to the official blog, outside scientists and developers can use Gemini 4 models with /teamwork and "/boost," for everyday coding, in Antigravity, and can also use DeepReview starting the same day. DeepReview is offered free to users up to twice a week. Google also opened applications for 10,000 academic researchers to use Antigravity's highest usage tier free for six months.
According to Mirrokni's post, Hydrogen models are available to everyone, while Carbon and Argon models are available to "Enterprise" and "Ultra/Paid" users. This breakdown by plan does not appear in the official blog. Neither the post nor the official blog gives the application period or how applicants will be selected.
Not every procedure is available externally yet. According to the official blog, the formal proof procedure and others will be added to Antigravity, and detailed tutorials will be posted on the Antigravity blog in the coming weeks. Mirrokni also said more details will be posted on the Antigravity blog.
The results are Google's own announcement, and the official blog links to paper postings and code repositories for many of them. It does not say whether they have been peer reviewed.
