Google's /teamwork results: 1.8 million lines of Lean for the Weil conjectures, a 2013 conjecture proved, and a Rust Zircon

On November 13, Google Research published a long results post on /teamwork, the multi-agent harness inside its Antigravity coding environment. Signed by Vahab Mirrokni, a Google Fellow and VP at Google Research, it lists what teams of Gemini 4 agents and human experts produced “over the past several weeks”: more than a dozen new results in mathematics and theoretical computer science, several very large Lean 4 formalizations, and rewrites of production C++ into Rust. Most of the claims link to an arXiv paper or a public repository, which makes this unusually checkable for a lab announcement.

The post matters less for any single theorem than for the method it describes, because the same pattern is now available to outside users: /teamwork, the /boost coding pattern and the Deep Review document checker are live in Antigravity, and Google is offering 10,000 academic researchers six months of free access at the highest usage tier.

How the harness is built: falsifiers and clean contexts

Google names two failure modes of long agent runs and designs around each. The first is that a single generation attempt is unreliable. The answer is parallel exploration paired with what the post calls dedicated falsifiers: an automatic judge that decides which candidates survive. The falsifiers it lists are the Lean 4 proof checker, unmodified software test suites, execution simulators, web search and hardware counters. If no objective judge exists for a task, this design has nothing to stand on, and the post is explicit that the approach is built around benchmarks, test suites and timers.

The second failure mode is attention degrading over multi-day tasks. Here the fix is context partitioning. Each specialized agent receives only the files and tools for one step, coordinators hand off to fresh successor agents, and critics and auditors check results from a clean context without seeing the producer’s reasoning. That last detail is the important one: a reviewer that inherits the author’s chain of thought tends to inherit its mistakes.

Workflows are written as declarative natural-language “patterns”, and a prompt is routed to the best fit. The named ones are Long Proof (an implementation of the Stellar Colosseum method), iterative coding (/boost), document review, a rewrite pattern for code migration, and DuoDiscover for ML kernels. The patterns are also revised from transcripts of past runs. One such review found that tightly coupled code does better with sequential implement-and-revise stages than with parallel splits, and /boost was changed accordingly.

Gemini 4 Argon is the model named for most campaigns. We covered its restricted rollout in our report on Argon.

The mathematics: one old conjecture and a stack of formalizations

The headline proof is the Courtade-Kumar conjecture, an information theory question from 2013. Send a random bit string through a noisy channel, then compress the output to a single bit: the conjecture says no function preserves more information about the input than a dictator function, which simply returns one of the bits. Researchers from Google, CUHK, USC and CMU report a proof in full generality. The division of labor is worth noting. Gemini first found counterexamples to a broader conjecture from an earlier CUHK paper. The CUHK team then proposed a candidate function that reduced the problem to a 14-variable optimization. The models partitioned the parameter space, produced most of the new analytic bounds and interval-arithmetic certificates, and extended the proof from balanced to unbalanced functions without human input. The result was then formalized in Lean 4.

Other results include near-optimal sample bounds for adaptive data analysis (a gap open since 2014), the first n-bit Boolean functions that need strictly more than n/2 quantum queries, a deterministic combinatorial algorithm for Boolean matrix multiplication that answers the main open question of a STOC 2024 paper, and a Lean-verified improvement on Tarjan’s 1985 deque conjecture for splay trees. Google calls the last one significant progress, not a resolution.

The formalization numbers are the largest published so far. A framework called LEAP, paired with Argon, turns informal proofs into machine-checked ones. Google says it produced an end-to-end formalization of the Weil conjectures of about 1.8 million lines of Lean across 28,800 subagent invocations, “fully autonomously”, plus more than 919,000 lines for a recent proof of Hilbert’s tenth problem over general rings of integers. In formalizing a recent proof of the 3D Bochner-Riesz conjecture, the system found and repaired a gap in the informal argument. For scale, the Fermat’s Last Theorem formalization we covered in an earlier post was treated as a landmark for the field.

One claim needs careful reading. The post says the system reproduced a formalization of a recent proof of finite-time blowup for 3D Navier-Stokes with smooth forcing. That is a formal check of someone else’s result on a variant of the problem. It is not a claim that the Millennium Prize problem is solved.

The engineering: Rust rewrites that got faster

The code results rest on the rewrite pattern, which exists because large migrations usually fail in two ways: agents stub out dependencies, or they edit the tests. The pattern schedules a module only after its dependencies compile, and links leaf modules against the original, unmodified test suite.

• Zircon, the Fuchsia microkernel: a two-week Argon campaign rewrote the remaining C++ on top of an earlier 25% port, adding about 800,000 lines of safe Rust that pass all kernel unit tests and boot on arm64 hardware.
• libgav1, Google’s AV1 decoder: about 170,000 lines of Rust with bit-exact parity on a conformance suite. The first port was roughly 4x slower than the C++. After the agents were given profiling tools and a speed mandate, the Rust version ran 20-30% faster than the original C++ and hand-written assembly on x86_64 and ARM.
• TPU kernels: full hardware evaluations of JAX/Pallas kernels take 7-32 minutes, too slow for search. Four parallel agents built 23-second proxy evaluators, checked them against periodic full runs using rank correlation, and reached a 4.09x geometric-mean speedup on 17 JAXBench kernels.
• Borg scheduling: two shipped changes cut TPU workload preemption by 24% on some hardware types.

Outside software, a 30-agent loop with a physics-informed spectral simulator identified molecular structures from NMR data with 95% top-1 and 100% top-3 accuracy, though the post does not name the benchmark or its size.

What the post does not tell you

There are no cost figures anywhere: no tokens, no compute hours, no dollars. For the Weil formalization there is no wall-clock time and no statement of how much rests on existing Lean libraries. There are no failure rates and no list of problems the harness attempted and did not solve, so the hit rate is unknown.

The human role is also larger than “fully autonomous” suggests. Researchers framed the questions and set constraints, and authors verified, simplified and edited the proofs for publication. For formal proofs the hard residual job stays with people: Lean confirms that a proof establishes the stated theorem, but only a mathematician can confirm that the formal statement says what the original conjecture meant.

The nearest thing to an external evaluation is Deep Review at STOC 2027. Authors of 578 submissions, more than a third of the total, opted in. Of 70 survey respondents, 90% rated the feedback mostly or almost entirely factual, more than 30% said it caught substantive proof bugs or significant typos, and 14% said it found gaps that took over an hour to fix.

What to watch

The rewrite pattern and the formal proof pattern are not yet available outside Google; the post says both are coming, with tutorials “in the coming weeks”. The more telling test is independent review of the linked papers. Lean-checked results stand on their own once the statements are audited, but several of the algorithmic results exist only as preprints or GitHub PDFs for now. If outside groups reproduce results of this kind using the public /teamwork, the claim shifts from “Google’s researchers did this with agents” to “the harness does this”, which is the claim that would matter to everyone else.