Google Details Antigravity /teamwork Maths Results

Google Research says its Antigravity /teamwork feature has been used, with human specialists, on a run of open problems in mathematics and engineering, and that it is opening the tools to external users. In a blog post dated 13 November 2026, Google Fellow Vahab Mirrokni presented the results as work from Antigravity’s “/teamwork multiagent systems, which enhance human-AI collaborations to solve open problems across mathematics, chemistry, systems software, and ML engineering.” Most of the work described is not yet peer-reviewed.

The flagship mathematical claim concerns the Courtade–Kumar conjecture in information theory, posed in 2013. Google says researchers from Google, the Chinese University of Hong Kong, the University of Southern California and Carnegie Mellon University used “/teamwork’s Long Proof pattern (implementing Stellar Colosseum in Antigravity) to prove information theory’s 2013 Courtade–Kumar conjecture in full generality.” The team, the post says, “formalized the entire proof in Lean 4, producing 50 million lines of code.” Gemini 4 Argon and earlier Gemini models, it adds, 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.”

That proof is set out in a 21 September 2026 preprint, arXiv 2609.24931, titled “A Proof of the Most Informative Boolean Function Conjecture.” The abstract describes a computer-assisted proof of the Courtade–Kumar conjecture and says the entire argument, including numerical certificates, “has been formally verified in Lean end-to-end.” It is a preprint, not a journal article. It is also not the only recent proof of the same conjecture. Two other independent proofs appeared on arXiv in the same period: 2609.24184, “Dictators are most informative,” by Vu Khac Ky and Tuan Tran, dated 21 September 2026, and 2609.26444, “The Most Informative Bit and Beyond: A Proof of the Courtade–Kumar Conjecture and Multibit Extensions,” by Hessam Mahdavifar and Ahmad Beirami, dated 22 September 2026. Google’s formalisation should be read alongside those papers, not as a unique settlement of the problem.

Mirrokni is explicit that the wider programme is collaborative. “All of this work is done in collaboration with human experts, and we are making these tools available externally.” The models named are Gemini 4 Argon, Gemini 4 Carbon and Gemini 4 Hydrogen, the last of which Google positioned for agentic workflows when it launched the model.

The same blog sets out further formalisation claims, with Lean line counts that TSN reproduces as Google stated them. It says /teamwork-LEAP “fully autonomously produced an end-to-end, machine-checked formalization of the Weil conjectures,” spanning “about 1.8 million lines of Lean, produced across 28,800 subagent invocations.” It also says the system “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.”

On Navier–Stokes, the wording needs care. Google says the system “independently reproduces an end-to-end formalization of a recent proof of finite-time blowup for the 3D Navier–Stokes equations with smooth forcing,” and notes that the equations are “part of one of the seven Millennium Prize Problems.” That is a formalisation of a recent proof for the equations with smooth forcing. It is not a claim, and TSN is not treating it as a claim, that the Millennium Prize problem has been solved.

The post also lists, as Google’s own account, first formalisations of the Birkhoff conjecture and the 3D Bochner–Riesz conjecture, the latter after “finding and fixing a gap in a recently released informal proof.” Those results, like later infrastructure claims in the same post, have not been presented here as independently peer-reviewed findings. Google says /teamwork workflows “have identified memory saving opportunities, surpassing our initial savings estimates of 1 PiB,” and that a Borg scheduling workflow “shipped 2 successful changes, resulting in a 24% reduction in TPU workload preemption on some hardware types.”

/teamwork, as described, is a multi-agent pattern that explores in parallel with “dedicated falsifiers,” including “the Lean 4 proof checker, unmodified software test suites, execution simulators, web search, or hardware counters,” and “partitions context by construction.” /boost is described as “a sequential solve-and-verify loop refined from prior trajectories.” Google says “many of these features are available in Antigravity” now, and that it will provide more updates “in the coming weeks” as it brings the remaining features to external users. It also says applications have opened for 10,000 academic researchers to receive six months of free access at the highest usage tier, and that “external scientists and developers can use Gemini 4 models with /teamwork and /boost in Antigravity and Deep Review today.” TSN previously covered Deep Review’s public release and, separately, cheminformatics skills added to the Antigravity agent.

Formalisations, preprints, and a problem that is not solved

The honest reading of the 13 November post is that Google is reporting a set of its own results, some of them already on arXiv, and opening a tool. It is not presenting a stack of journal theorems, and it does not claim that an AI system proved Courtade–Kumar alone. The 50 million Lean lines are a machine-generated formalisation of a proof developed with human experts. Line counts of that size measure formalisation volume; they are not a proxy for conceptual novelty or for peer review.

The two other Courtade–Kumar preprints are a useful check on any temptation to treat the Google–CUHK–USC–CMU paper as unique. Independent proofs can coexist, and they can differ in method, generality and the amount of computer assistance. Until the literature settles, the responsible stance is to name all three and wait for referees.

The Navier–Stokes sentence is the one most likely to be repeated carelessly. A formalisation of a recent proof of finite-time blowup with smooth forcing is a verification task. The classic Millennium Prize problem concerns, among other things, the unforced equations in three dimensions. Google’s own phrasing is about reproducing a formalisation of a recent, forced result. That is not a solution of the prize problem.

A comparison with OpenAI’s publication of 372 AI maths results, about 42 per cent of them Lean-checked, is useful only at the level of method. Both laboratories are now putting large Lean artefacts into public view. Neither practice, on its own, converts a preprint or an internal formalisation into a refereed theorem.

The access offer — 10,000 academic researchers, six months, highest usage tier — will matter if the remaining /teamwork features do arrive “in the coming weeks” as promised. Until then, outsiders have Google’s account of what the internal collaborations achieved, a Courtade–Kumar preprint that sits beside two others, and a clear warning not to read a forced Navier–Stokes formalisation as a Millennium Prize solution.

Sources

Vahab Mirrokni, Google Research, “Advancing science & engineering with Antigravity’s /teamwork,” 13 November 2026, https://research.google/blog/advancing-science-engineering-with-antigravitys-teamwork-feature/
Zijie Chen, Amin Gohari, Adel Javanmard, Honghao Lin, Vahab Mirrokni, Chandra Nair and David P. Woodruff, “A Proof of the Most Informative Boolean Function Conjecture,” arXiv 2609.24931, 21 September 2026, https://arxiv.org/abs/2609.24931
Vu Khac Ky and Tuan Tran, “Dictators are most informative,” arXiv 2609.24184, 21 September 2026, https://arxiv.org/abs/2609.24184
Hessam Mahdavifar and Ahmad Beirami, “The Most Informative Bit and Beyond: A Proof of the Courtade–Kumar Conjecture and Multibit Extensions,” arXiv 2609.26444, 22 September 2026, https://arxiv.org/abs/2609.26444