Google's /teamwork math claims, checked: 99.5% of the 50 million Lean lines are certificates, and the Weil formalization isn't public

Google Research's November 13 post on Antigravity's /teamwork, "Advancing science & engineering with Antigravity's /teamwork" by Vahab Mirrokni, reads like a highlight reel. Multi-agent "campaigns" on Gemini 4 Argon proved the 2013 Courtade–Kumar conjecture, "formalized the entire proof in Lean 4, producing 50 million lines of code." A system called /teamwork-LEAP "fully autonomously produced an end-to-end, machine-checked formalization of the Weil conjectures," about 1.8 million lines of Lean from 28,800 subagent invocations. There are another dozen math results, a Zircon microkernel port that adds about 800,000 lines of safe Rust, a 9x9 Go engine trained from scratch and fleet-wide memory savings at Google.

We checked the two claims that made the headlines. One holds up better than the post's own numbers suggest. The other can't be checked at all, and a public formalization of the same theorem appeared a week earlier, from someone else.

Courtade–Kumar: real, audited, and from September

The Courtade–Kumar proof isn't new. "A Proof of the Most Informative Boolean Function Conjecture" (arXiv:2609.24931), by Zijie Chen, Amin Gohari, Adel Javanmard, Honghao Lin, Vahab Mirrokni, Chandra Nair and David P. Woodruff, went up on September 21. Nor was it the only proof. Vu Khac Ky and Tuan Tran posted a different one the same day (arXiv:2609.24184), Hessam Mahdavifar and Ahmad Beirami followed on September 22 with a proof whose one-bit part, by their own disclosure, "was developed by generative AI under our high-level direction", Dimiter Kramer and Mert Saglam of DeepInfra published another, and OpenAI released two more in October. Mirrokni acknowledged Ky and Tran in September, when he announced the result. The November post mentions none of them.

What sets Google's version apart is the formal proof, and that part is real. We cloned dpwoodru/general-courtade-kumar-lean and counted: 45,510 .lean files, 50,373,106 lines. The "50 million" checks out. But the repository's own guide says only 1,359 files, 238,690 lines, are readable proof code. The other 44,141 files (4.88 GB) are generated certificate data, numerical bounds over pieces of the parameter space that the Lean kernel checks, mostly with decide. Under half a percent of the line count is the proof a person would read. The rest is the interval arithmetic.

The audit trail is better than for most formal-math announcements. What a human has to trust is a 63-line statement, GeneralCK/Statement.lean. The README records a clean rebuild with a byte-identical final .olean, an independent run of the verification kit, acceptance by Lean's comparator against the statement in google-deepmind/formal-conjectures, and acceptance of all 22,107,215 declarations by con-leche, the Lean FRO's external checker. All of that happened between September 23 and October 15. In November it is a well-documented old result with a large number attached.

The Weil conjectures: no code, and a public version from Axiom

For the Weil formalization the post links to Wikipedia pages for the Weil conjectures and Pierre Deligne. There's no repository, no paper and no statement file. The same goes for the rest of the LEAP paragraph: the 919,000 lines for Hilbert's tenth problem over rings of integers, the "first formalization" of the Birkhoff conjecture, the 3D Bochner–Riesz conjecture (with a gap "found and fixed" in an informal proof), and the reproduction of a Navier–Stokes blowup proof. LEAP itself links to a framework paper (arXiv:2606.03303), not to any of these. We found no Weil or LEAP repository under Google's GitHub organizations.

Axiom published AxiomMath/Weil on November 6, a week before Google's post, under Apache 2.0. It states and proves all four Weil conjectures (rationality, the functional equation, the Riemann hypothesis over finite fields and the Betti-number statement), following Freitag and Kiehl's Étale Cohomology and the Weil Conjecture. Its README says there is no sorry, no native_decide and no added axiom. A static scan we ran found no sorry in the code either. Carina Hong, Axiom's founder, said it took less than a day. Google's post doesn't mention Axiom.

Axiom's version also shows why "1.8 million lines" can't be compared with anything on its own. We counted 213,159 lines in AxiomMath/Weil, about 980 modules that the README says were "written by AI agents" and "not yet reviewed by humans." They sit on Axiom's Lean formalization of the Stacks Project, which we covered on November 5. Back then neither Axiom's post nor the README gave the split between its human-reviewed and AI-written tiers. Counting the repository as of November 14 answers that: the AI-written StacksFrontier tier is 18,356,552 lines, the human-reviewed StacksCore tier 37,378, about 0.2% of the total. Deligne's key weight estimate isn't in the Weil repository at all; it comes from Stacks, proved along Laumon's later Fourier-transform route. So depending on where you draw the boundary, Axiom's Weil formalization is 213,000 lines or 18.6 million.

Google's 1.8 million could be either kind of number: a self-contained development from Mathlib, or a thin layer over foundations nobody outside has seen. Until the code is out, nobody can say which theorem it states, which axioms it uses, whether it rebuilds, or how much it overlaps with work that was already public. "Fully autonomously" is also hard to weigh when the formal statement it was aimed at isn't published.

Which results you can check

The rest of the post is uneven in the same way. Some results come with artifacts: the combinatorial Boolean matrix multiplication algorithm (arXiv:2611.06717, with a Lean formalization in lockqueue/bmm), the integer multiplication work (lockqueue/intmul), the splay-tree deque bound (sorrachai/SplayTree-Deque-Ordinal-Inverse-Ackermann-Bound, in Lean) and the Steiner spanner lower bound (goranzuzic/high-dimensional-steiner-spanners, in Lean), plus arXiv papers for the quantum query, sketching and cut-sparsification results. The LEAP formalizations, the Zircon and libgav1 Rust ports, the Go engine and the Borg scheduling changes have no public code linked.

The part worth keeping

The engineering idea under all of this is clearer than the scoreboard. /teamwork pairs parallel attempts with "falsifiers" that decide which candidate works: the Lean checker, unmodified test suites, simulators, hardware counters. It partitions context on purpose, so each agent gets only the files and tools for its step, and critics review results from a clean context without the producer's reasoning. The patterns are declarative natural-language workflows that the system routes prompts to. One detail stands out: a long campaign that analyzed past run transcripts concluded that tightly coupled code is better handled by sequential implement-and-revise stages than by parallel splits, and that finding went into /boost. That's a harness tuning another harness, and it's the most transferable thing in the post.

It also explains the Courtade–Kumar repository. Forty-four thousand files of certificates are what you get when the falsifier is a proof kernel and the agents are allowed to grind. That's a perfectly good way to prove an inequality. It just means the line count measures how hard the checker was worked, not how much mathematics was done. For Weil, Google hasn't shown either.