Google Says Its AI Agents Rewrote a Landmark Math Proof as Code a Computer Can Check

Google Research said on Nov. 13, 2026, that teams of its AI agents produced a complete, machine-checked version of the Weil conjectures, the landmark results on counting solutions of polynomial equations in finite number systems. The proof itself dates to 1974, when Pierre Deligne completed it. What the agents produced is that existing proof rewritten in Lean 4, a language that turns a proof into code a computer checks line by line.

In its announcement, Google gives its reason: checking a computer-assisted proof by hand is heavy work for peer reviewers, and small flaws can hide inside long calculations. Once mathematicians have confirmed that the formal statement matches the original problem, the code compiles only if every logical step holds.

The formalization runs to about 1.8 million lines of Lean, produced across 28,800 separate agent calls, and Google describes the run as fully autonomous. The company does not say whether that code has been released. The same framework also produced what Google calls the first formal version of a recent proof of Hilbert's tenth problem over general rings of integers. All of these figures are Google's own account of its own system, and no outside group has reproduced the runs.

One result in the post is new mathematics, separate from the formal rewrites described above. Google says a team that included researchers from the Chinese University of Hong Kong, the University of Southern California and Carnegie Mellon University proved the Courtade-Kumar conjecture in full generality. That question in information theory had been open since 2013. The post splits the credit: the models found counterexamples to a generalized version and developed most of the new bounds, and the academic team proposed the candidate function and the key bound they built on.

Google said the campaigns ran on its Gemini 4 models, among them Gemini 4 Carbon. The agent tools are now available to outside developers in Google's Antigravity environment, and the company has opened applications for 10,000 academic researchers to get six months of free access to its highest usage tier.