Google says its Gemini 4 agent teams proved a 13-year-old information theory conjecture
Google Research also claims results on other open problems, many checked in Lean. They are Google's own preprints.
On 13 November 2026 Google Research described results from Antigravity’s /teamwork, a tool that runs several AI agents on one problem, mostly built on Gemini 4 Argon. Some agents propose solutions and others try to break them. The post links a series of preprints (papers not yet peer reviewed), most written with university researchers.
The headline result is the Courtade–Kumar conjecture, posed in 2013, about how much information a yes/no function of noisy data can carry. Researchers from Google, CUHK, USC and CMU say the agents helped prove it in full. The arXiv paper calls it a computer-assisted proof, and the team formalized it in Lean 4, a language in which a computer checks every step, in 50 million lines of code.
The post lists other claims. A bound on adaptive data analysis, open since 2014, was proved and checked in Lean. A 2014 question about quantum queries was answered. A new algorithm settles the main open question of STOC 2024 on Boolean matrix multiplication. A bound for Tarjan’s deque conjecture was also checked in Lean.
A second system, LEAP, produced Lean formalizations of the Weil conjectures (about 1.8 million lines, 28,800 subagent invocations) and of Hilbert’s tenth problem over general rings of integers (over 919,000 lines). Google says an application form gives 10,000 academic researchers six months of free access.
What it means
If the results hold, agent teams are now producing proofs on problems that stood open for years, in a field where a computer can check the answer. The post gives no verdict from outside referees, and the arXiv papers are the first place to look.
Caveats
- Google reports its own results, and the post does not say whether any have been peer reviewed. Labs publish successes more readily than failures.
- A Lean check proves the Lean statement. It does not show that the statement matches the problem as mathematicians pose it.
- The post says humans verified, simplified and edited some of the algorithms for publication, and it does not separate what the agents did from what the researchers did.
- We read the Courtade–Kumar abstract only, and did not check the proof or the Lean code.