Google's AI agent teams help prove a mathematical conjecture from 2013

On Friday, Google reported new results from /teamwork, a feature in Antigravity, Google's programming platform in which AI agents carry out work on their own. On Tuesday 10 November, Google already had a team of AI agents programming together in Antigravity with /swarm. With /teamwork, such teams work not only on code, but also on mathematical research.

In /teamwork, the agents are given different roles. One works out a solution, another looks for mistakes, and an agent that gets stuck hands its task over to a new one. Human experts set the questions and judge the results. For the new results, Google mainly used Gemini 4 Argon, its most powerful AI model, which it released at the end of October 2026. According to Google, the work was done over the past few weeks.

An old conjecture proved

In mathematics, a conjecture is a statement that many researchers believe to be true, but that nobody has proved yet. The Courtade-Kumar conjecture from 2013 is about a sequence of ones and zeros of which a copy has been damaged by noise: here and there a 1 has become a 0, or the other way round. How much can one single result, calculated from the original sequence, reveal about that damaged copy? The conjecture says that the most is revealed when that result is simply one of the original ones or zeros. The question matters for the theory of how information gets through a noisy connection.

Researchers from Google, the Chinese University of Hong Kong, the University of Southern California and Carnegie Mellon University proved the conjecture together with the AI agents. The proof appeared in September 2026 as a preprint. The researchers from Hong Kong came up with the approach that reduced the problem to a calculation with fourteen unknowns. According to Google, Argon and earlier Gemini models then worked out most of the calculation steps and checks that were needed.

The entire proof has been converted into 50 million lines of Lean, a programming language that lets a computer check every logical step of a proof. Around the same time, other mathematicians also put proofs of this conjecture online.

Famous proofs checked as well

Google also reports that /teamwork with Argon converted the Weil conjectures into Lean entirely on its own, in about 1.8 million lines. These conjectures about counting the solutions of equations were already proved in 1974 by the Belgian mathematician Pierre Deligne. So what is new is not the proof itself, but that an AI system put such a large and famous proof, without help, into a form that a computer can check.

Earlier, in August 2026, Google had already shown that agent teams using the older Gemini 3.1 Pro solved seven open problems in theoretical computer science. Human experts approved six of them; the seventh proof, more than forty pages long, was checked by the computer in Lean.

Developers with a paid subscription can use /teamwork themselves in Antigravity. Google is also offering 10,000 university researchers six months of free access to the most powerful version.

What does this mean for the road to the singularity?

Computers that check every step of a proof have existed for a long time. The problem was that someone first had to write out all those steps, and that sometimes took mathematicians years. If AI agents do that writing themselves, millions of lines at a time, such a check becomes cheap. A mathematician can then deliver a computer check together with a new proof, so that colleagues do not have to spend months working out whether it is correct.

If that trend continues, it also helps AI itself move forward. A proof that the computer has approved is an answer that is certain to be right. An AI model that learns from such answers can take on harder and harder problems without a human having to check every answer. Other AI companies will then also have to show that their models deliver work a computer can check, and not just text that sounds convincing. People will still be needed to choose which questions are worth the effort, and to make sure that the statement the computer checks really describes the problem they meant.

What is the technological singularity? Read the explanation →