Google's AI agents wrote 1.8 million lines of Lean to machine-check the Weil conjectures

A proof that took mathematicians decades to complete has now been translated by a crew of AI agents into roughly 1.8 million lines of code that a computer can check line by line. In a Nov. 13 post, Google Research vice president Vahab Mirrokni wrote that Google's multi-agent system /teamwork-LEAP fully autonomously produced an end-to-end, machine-checked formalization of the Weil conjectures, using about 28,800 subagent calls. At 50 lines per printed page, that code would fill about 36,000 pages.

The Weil conjectures describe how many solutions polynomial equations have over finite fields. They are a landmark of algebraic geometry, finally proved by Belgian mathematician Pierre Deligne in 1974. Proofs at this level run for hundreds of pages, and referees struggle to check every step. Lean 4 is a proof assistant: once a proof is written as code and mathematicians confirm the theorem statement is right, the code only compiles if every logical step holds.

The post lists more. The system wrote more than 919,000 lines of Lean to produce the first formalization of a recent proof of Hilbert's tenth problem over general rings of integers. It independently reproduced a formalization of a recent proof of finite-time blowup for the 3D Navier-Stokes equations with smooth forcing. It produced the first formalization of the Birkhoff conjecture, posed in 1927, and while formalizing the 3D Bochner-Riesz conjecture it found and fixed a gap in a recently released informal proof. Working with teams including the Chinese University of Hong Kong, Google also proved the 2013 Courtade-Kumar conjecture in information theory, with a Lean proof of 50 million lines. Google says human experts were involved throughout.

The trick is division of labor plus cross-examination. A single model tends to drift over very long chains of reasoning, so /teamwork splits the job into small pieces. Each agent gets only the files and tools its step needs. Separate critics and auditors recheck results from clean contexts, without seeing the original agent's reasoning, and the Lean checker has the final say. Think of a construction crew where each team gets only the blueprint for its own floor, and the inspector ignores the builders' explanations and just brings a tape measure.

For comparison, the startup Axiom announced its own Lean formalization of the Weil conjectures on Nov. 6, built on the community library Mathlib; Google's emphasis is that its version was produced autonomously by the system. The same tools rewrote libgav1, Google's AV1 video decoder, from C++ into about 170,000 lines of Rust with bit-exact output, and after tuning the port ran 20% to 30% faster than the original. A team of 30 agents identified molecular structures from NMR data with 95% top-1 accuracy on hard benchmark molecules. Formal checking confirms that an existing proof is airtight; mathematicians still have to confirm that the formal statement matches the original theorem. Google has opened /teamwork and /boost in Antigravity, is offering 10,000 academic researchers six months of free top-tier access, and says its formal-proof pattern will arrive in a later update. Chinese teams are on the same path: ByteDance's Seed-Prover and DeepSeek's Prover models also use Lean for automated theorem proving and posted results in 2025 on International Mathematical Olympiad problems and benchmarks such as PutnamBench.

Original publication time: Google Research blog, Nov. 13, 2026 (US Eastern); Interesting Engineering, Nov. 14, 2026 10:34 Beijing / Nov. 13, 2026 21:34 EST; IT Home, Nov. 14, 2026 14:53 Beijing / Nov. 14, 2026 01:53 EST