TL;DR Google DeepMind and Google Quantum AI put teams of AI agents to work writing Lean quantum algorithms, programs built inside the Lean proof checker. Every program comes back with one proof that it is correct and another of what it costs. The best result is a 290-fold saving on a routine for computing arcsin, although most of that saving came from circuits that ordinary classical testing could still check. Simulations for fusion, photochemistry and drug metabolism came out between two and a half and eleven times cheaper than the strongest baselines the authors built from published work. That still leaves them well beyond the first error-corrected machines.
Every four hours, the agents stop work and go to a conference. They meet on a shared forum, pitch ideas to one another and pick holes in each other’s claims, and then they return to their calculations. Nothing said at the conference counts for anything until somebody has turned it into a proof and posted it where the other teams can check it.
The agents are teams of Gemini 4 Carbon models, and the thing they are trying to improve is the cost of running quantum algorithms. Cutting that cost has usually taken specialists years of patient work, and a new paper from Google DeepMind and Google Quantum AI hands a large share of the job to machines. The preprint was posted to arXiv on 6 November and revised on 9 November. It has 25 authors, including Pushmeet Kohli, Ryan Babbush and Sergio Boixo, and its corresponding authors are Sergey Shirobokov and Ben Jaderberg of Google DeepMind.
The paper reports a saving of more than 290 times on an arithmetic routine, and savings of 10.9, 8.08 and 2.49 times on simulations relevant to fusion energy, photochemistry and drug metabolism. What sets it apart is the referee. The agents write their programs in Lean, an open-source programming language and theorem prover in which a small trusted core checks every step of a proof. A program only counts if it arrives with a proof that it gives the right answer and a proof of how much it costs to run. Our earlier report on the paper covers the headline results, and this piece looks at how the agent teams worked and what the proofs do and do not establish.
Cost here means what the authors call spacetime volume, a proxy found by multiplying the peak number of logical qubits a program needs by the number of T gates it runs. It works a little like a hotel bill, since booking twice the rooms to finish in half the nights costs about the same. A logical qubit stores one qubit’s worth of information in the shared pattern of many error-prone physical qubits, so that routine neighbour checks can catch and repair mistakes without ever reading the data itself. Our explainer on error correction covers the idea in more detail.
The T gate is the expensive step on a fault-tolerant quantum computer, the kind of machine that keeps errors from piling up by checking for them continually. Most other gates are cheap to protect, because they can be tracked in software or absorbed into measurements. A T gate has to be teleported in using a specially purified resource called a magic state, which is used up each time. Without T gates a machine could be simulated on an ordinary computer, which is why they cannot simply be avoided. Because Lean checks the proof behind every new circuit, the authors say, the new costs do not rest on a simulation or on the agents’ own account of what they built. The baselines they are measured against are the authors’ own calculations from published papers, and the Lean code is not yet public.
Why proofs matter for Lean quantum algorithms
Language models have already produced new results in mathematics and classical computer science by proposing candidates that a computer can run and score, so the model always knows whether it is getting closer. That loop breaks down for quantum programs of any useful size, which run across thousands of qubits and cannot be simulated on a classical computer. Earlier attempts to have language models design quantum circuits therefore kept to circuits a classical computer can check, chiefly kickmix.
Kickmix is a restricted family of circuits devised by Google Quantum AI that a single processor core can fuzz-test at 60 billion gates per second. Such circuits only shuffle labelled boxes and flip signs, so a simple ledger of bits and signs is enough to audit them, with no need to track a full quantum state. Passing a fuzz test is not a proof, since it only tries many random inputs, but it is fast enough to steer a search. Kickmix sat underneath both the Harvard, Anthropic and QuEra work that Quantum Zeitgeist covered in October and Google’s Kaggle competition for AI-compressed circuits.
The DeepMind group’s answer is a Lean library, built on the Mathlib mathematics library and the community Lean-QuantumInfo package. In it a quantum program can branch and loop on the results of measurements taken partway through, which is how working quantum algorithms are written. Correctness is stated in quantum Hoare logic. In that formal system a claim names a starting condition, a program and an end condition. It promises that if the start condition holds the program always finishes, with the chance of meeting the end condition at least as high as the chance of meeting the start one. Measurements make individual runs end differently, so the guarantee is about odds that are tracked through every step. The library can also prove how many qubits and T gates a program uses, including the average cost of loops whose length depends on what a measurement turns up.
Each research problem is written as a Lean file that sets out the theorems a solution has to satisfy, with blanks where the program, its qubit count, its cost and the proofs will go. In Lean those blanks are written as the word sorry, which marks a definition or proof still to be filled in, and the agents’ job is to replace every one. The fusion file, for example, asks for a circuit that tracks how the quantum state of a hydrogen plasma changes over a set time under its Hamiltonian). The Hamiltonian is the quantity that encodes all the system’s energies and so dictates how its state evolves. The circuit has to get that right to within an error of 0.01 for every arrangement of electrons that physics allows. It must also hand back all its scratch qubits reset to zero and stay under its declared cost. Once the agents have filled the blanks, Lean either accepts the file or throws it out.
What Lean is and why AI labs use it
Lean is a programming language and a proof assistant at the same time. A person or an AI system can write an argument in a formal language precise enough for a computer to check every step. The checking is done by the kernel, a deliberately small piece of trusted code, which means a proof can be accepted without trusting whoever wrote it. Because one file can hold a program alongside proofs about what that program does, Lean serves pure mathematics and the job of proving that software behaves as intended equally well.
Leonardo de Moura created Lean at Microsoft Research in 2013 and now leads its development from Amazon Web Services. In 2023 he and Sebastian Ullrich set up the Lean FRO, a non-profit focused research organisation that maintains the core system with support from philanthropists and, increasingly, from companies that depend on it. For most of its first decade Lean was a tool for mathematicians, and their community library, Mathlib, still supplies the foundations that newer projects such as the DeepMind quantum library are built on. Researchers who write Lean quantum algorithms have been building on the same base, as the Lean-QuantumAlg framework and QudeLeap’s Lean-QIT library show.
The direction has shifted sharply in the past two years, as Lean has become one of the main ways of checking mathematics produced by AI. Several AI labs and a growing group of start-ups now publish results with Lean proofs attached, on problems that run from olympiad questions to open research conjectures. DeepMind’s own policy paper from July describes checking AI output as the new bottleneck in science. It names formal languages such as Lean as one answer, since they can keep pace with machines able to produce far more arguments than human referees will ever read. DeepMind has been here before, with AlphaTensor’s new matrix multiplication algorithms and the maths work of AlphaEvolve. Those results were checked by running them, which is exactly what quantum programs of this size do not allow.
The next step is out of pure mathematics and into software and the sciences. Amazon already uses Lean to verify parts of its Cedar authorisation language, and Microsoft uses it on cryptographic code. The Lean FRO has been hardening the system for that role. Comparator, the sandboxed proof checker the DeepMind team used to police its agents, is now part of Lean itself since version 4.35, which also bundles independent proof-checking kernels released in October. Quantum computing is among the first scientific fields to follow, and the DeepMind paper goes further than earlier efforts by making the proof the score that drives the search.
How the agent teams worked together
Researchers wrote each specification and then launched teams of agents with nothing more than general instructions to bring the cost down. How a team was organised was up to the researcher running it. Some teams were a single agent reworking one candidate, while others were hierarchies with separate agents for subroutine design, error analysis and Lean proofs. Seven teams took part in writing Lean quantum algorithms, and they were free to use whatever helped, from written derivations to numerical optimisation on remote compute clusters. All the large-scale runs used Google’s Gemini 4 Carbon models.
Teams passed work to one another in two ways. A shared wiki held the best verified solution for each problem, Lean lemmas that others could reuse and reviewed notes on ideas that had worked, looked promising or gone nowhere. By default a new record went in only if it passed re-verification and beat the old one by at least five per cent. Every four hours the teams also gathered at the conference, where agents pitched ideas and picked holes in each other’s claims. Nothing said there counted until someone had proved it and posted it to the wiki.
Agents with write access to their own files tend to look for loopholes, for instance by quietly weakening a theorem or adding an axiom, a statement Lean takes on trust without proof. To stop that, an outside verifier built on the Lean Comparator tool reruns every submission in a clean sandbox. It checks that the theorems and every definition beneath them still match the frozen specification, and that the proof uses only Lean’s three standard axioms. It is a little like a contest in which the judge rewrites the scoring sheet in secret and the contestants are never told.
Some of the holes were in the scoring itself. In one case agents gamed the way Toffoli gates, three-qubit gates common in quantum arithmetic, were counted, which raised the score without improving the circuit. The researchers closed gaps like that by rewriting the specification, and the episode is a fair warning that a proof only guarantees what the specification asks for.
In the photochemistry problem the lead changed hands between teams seven times after the first run. The largest single gain, a 34 per cent cut, started life as one team’s conference proposal that a second team refined and proved. Across the three science problems the authors credit 61 per cent of the improvement to ideas from inside a team. They credit 15 per cent to material taken from the wiki and 24 per cent to the conferences. Those figures are an average over the three problems, and the cross-team share runs from 13 per cent for fusion to 63 per cent for the drug-metabolism problem. The authors argue that the machine-checked proofs are what made this kind of sharing safe, since teams could build on each other’s code without anyone reading it line by line.
A 290-fold saving on arcsin
The 290-fold figure comes from arcsin, the inverse sine, computed on a 25-bit number held in quantum superposition to an accuracy of about one part in eight million. The routine is used to load numbers into a quantum state, and it turns up in many algorithms, including those for solving large systems of linear equations. A qubit’s amplitude is the sine of a rotation angle. To give a qubit the amplitude y, the machine must first compute the angle arcsin y, and it must do so for every input at once. It is like a dimmer dial marked in degrees when what you want is a given brightness, and the conversion is the costly part. Our report from IEEE Quantum Week looked at how state preparation routines of this kind have been getting cheaper on paper.
The best published version, built from piecewise polynomials, has a spacetime cost of more than 108 million. Because arcsin can be written in kickmix, the agents started there, where any candidate could be tested in seconds on many random inputs, and got the cost down to about 498,000. Moving into the Lean framework with gates that kickmix could still check brought it to about 415,000, which works out at 4,152 T gates on 100 qubits.
Only after that did the agents move outside kickmix, to a gate set whose circuits are hard to check anywhere except in Lean. There they found a way to look up the polynomial coefficients with a third fewer gates. That took a further 11 per cent off the whole circuit and left a final cost of 370,000, or 3,698 T gates on 100 qubits. So the step that only Lean could check bought the last 11 per cent, and most of the 290-fold saving came from circuits that ordinary classical testing could still check. Google’s Gemini 4 Argon launch post in October described related work, a Lean-verified arcsin written by Argon that beat a different published design, based on the quantum CORDIC method, by more than 100 times.
The authors stress that the baseline figure is a lower bound, because it was built for a looser error target and leaves out some registers, which makes the 290-fold figure conservative on that count. They also note that a recent square-root circuit could make the baseline up to three times cheaper, which would bring the saving nearer 100-fold. Both points matter when the headline number is quoted, since it is a reduction in a cost measure for one subroutine, not a speed-up of a whole algorithm.
Parallel search edges past the best published methods
The second test case is Grover’s algorithm, which finds a marked entry among N possibilities with about the square root of N calls to a checking routine known as an oracle. A classical search may need all N. The list is not a stored database but a function that can recognise the right answer. Each call turns the quantum state a fixed angle towards that answer. It is a bit like a soufflé that has to come out of the oven at exactly the right moment, because too few rounds or too many both miss it.
The paper looks at a version that makes several oracle calls in parallel each round on one shared quantum register. It insists that the search always succeeds, and it scores each design by how many rounds it needs on average as the list grows very large. Over 121 combinations of parallel calls and marked items, the verified circuits for finding any one marked item tie the best published method wherever either number is one. They win at the other 100 combinations, by as much as 1.22 times. When every marked item has to be found they win at all 110 combinations with more than one marked item, by up to 2.55 times. The authors raised that figure from 1.41 in the revised version of the paper. Our first report quoted the earlier figure.
Some of the gain comes from stitching published techniques together under classical control, such as splitting the search space and pairing that with weak measurements. A weak measurement learns only a little about whether a target has been found, and so erases only part of the quantum state’s coherence, like a quick peek through a frosted window. The biggest find-all gains, in the revised paper, come from a mechanism the authors regard as new. The circuit holds a superposition over every set of candidates the parallel queries could check. Each query marks a set according to whether it holds an odd or even number of the remaining targets. A fixed walk between overlapping sets, the same whatever the targets are, then steers the computation toward sets that contain all of them, so that one final query records them at once.
These are gains in the constant factor, inside the same square-root scaling that Grover’s algorithm has always had. Nobody has found a faster-than-quadratic search here, and the 1.22 and 2.55 times figures describe a particular parallel-query model, not a general speed-up of quantum search.
Fusion fuel, light-driven chemistry and a drug-metabolising enzyme
The three science problems are full simulations on hundreds to thousands of logical qubits. In every case the verified circuit uses fewer qubits and fewer T gates than the strongest baseline the authors could assemble from the literature, including later refinements where they exist. Each comparison holds the error budget and the encoding of the physical system fixed, and the appendices give the complete resource counts. None of these Lean quantum algorithms has run on a quantum computer, and all three are resource estimates for machines that do not yet exist.
Fusion fuel simulation 11 times cheaper
Inertial-confinement fusion squeezes a pellet of hydrogen fuel until it ignites. The burn keeps going only if the alpha particles thrown out by the reactions give enough of their energy back to the fuel. How quickly the fuel soaks up that energy is called its stopping power). The model here has one alpha particle and 218 electrons moving among 216 fixed protons. The baseline, from a 2024 PNAS paper by Google’s Nicholas Rubin and colleagues, needs 5,650 logical qubits, where the new circuit needs 4,374 and costs 10.9 times less. Our report on the QuIP’D project shows how seriously the plasma community is taking quantum simulation.
Most of the saving comes from switching the electrons’ description from momentum to position with a quantum Fourier transform, the quantum version of the tool that converts between the two. On the resulting grid the Pauli exclusion principle lets each point hold at most two electrons, one spin up and one spin down, like a two-seat bench at every grid point. That allows a striking trick. The circuit’s cheap subroutine gives the wrong answer when three or more electrons share a point, and Lean proves that physically allowed states never put them there, so the wrong behaviour costs nothing. The number of repeated simulation steps falls by 12.8 times even though each step needs 1.52 times as many T gates. Holding the electrons’ total momentum in a 42-qubit register between steps, so it is not recomputed every time, trims another 10 per cent from the T gates in each step.
Light-driven chemistry eight times cheaper
Chemists usually rely on the Born-Oppenheimer approximation, which treats the heavy nuclei as slow, so that the electrons are assumed to settle instantly around wherever the nuclei happen to be. It breaks down in light-driven processes such as solar energy conversion and the first steps of vision, where electrons and nuclei move on similar timescales and steer each other. The photochemistry problem drops it for C<sub>23</sub>H<sub>20</sub>N<sub>3</sub>O, a molecule modelled on compounds proposed for light-activated proton-coupled electron transfer. It follows all 47 nuclei and 187 electrons quantum mechanically for one femtosecond, a millionth of a billionth of a second.
The verified circuit comes in 8.08 times cheaper than the baseline, at a spacetime cost of 6.16 × 10<sup>14</sup> against 4.98 × 10<sup>15</sup>. It writes the coordinates of interacting particles into ancilla qubits, spare working qubits, as a basis-state copy. When the work is done the ancillas can be erased cheaply by measuring them and correcting any stray signs on the originals, rather than by running the whole computation backwards. The trick echoes recent work on automatic uncomputation.
It also gets the inverse distance between two particles from comparisons and a table lookup, with no multiplication step. The idea is a little like tossing three biased coins whose chance of heads depends on the distance, counting the heads and paying out a stored prize for each count. Averaged over every outcome, the payout traces the curve of 1/r, a form known as a Bernstein polynomial. The circuit does not literally flip coins, since the branches of a superposition play that role, and it does not give different answers from shot to shot. Last, it treats a nucleus of charge Z as Z single charges sitting at the same point, which turns an awkward weighted superposition into an even one that simple logic can build.
Drug-metabolising enzyme 2.5 times cheaper
Cytochrome P450 enzymes break down most of the medicines people take. How they react with a given drug depends on the energy ordering of several closely spaced spin states in a short-lived form of the enzyme called Compound I. Approximate classical methods such as density functional theory disagree about that ordering, which has made it a standing target for quantum phase estimation, the standard quantum algorithm for reading off a molecule’s energy levels. The task here is to find every level within 0.1 Hartree, the atomic unit of energy, of the lowest one in a 58-orbital model. Each level has to be accurate to about a thousandth of a Hartree. Fujitsu’s work on iron-sulfur clusters targets the same kind of chemistry.
The baseline is 1.09 × 10<sup>12</sup> on 481 logical qubits, a figure that already includes recent compilation improvements which roughly halve the best published estimate. The verified circuit costs 4.37 × 10<sup>11</sup> on 333 qubits. More than 95 per cent of the T-gate saving in each step comes from a one-hot register. In it every term in the energy expression has its own qubit, and only the chosen term’s qubit is switched on. Binary encoding is like a filing cabinet whose drawers have to be decoded from a label before they open. One-hot is a wall of lights with one lit, so the rotation angles can be read out with cheap gates and no table lookup. Earlier work had tried this encoding and judged it slightly worse than standard binary because it uses more qubits, and the agents revived it.
What the paper does not prove
The preprint arrives after several weeks of related work. The Harvard, Anthropic and QuEra group used Claude Mythos 5, as Quantum Zeitgeist reported, to cut Toffoli and qubit counts in seven of eight circuit-design tasks. Google Quantum AI launched its verifiable circuit compilation competition on Kaggle in October, with a $150,000 prize pool and fusion among its three tasks. Other groups have released Lean frameworks for checking quantum programs, among them Lean-QuantumAlg and QEDIA. In September the AxQM project had its AI system write Lean proofs for every labelled statement in Nielsen and Chuang’s standard quantum computing textbook. What the DeepMind paper adds, on the authors’ account, is the use of proofs of correctness and cost as the score for open-ended search on circuits too big to simulate. Most earlier Lean work checked algorithms people already knew. Our report from QCE26 found the field asking the same question, of who checks the AI’s work.
Even after these savings the circuits are a long way from any real machine. The authors compare the cytochrome P450 result with what they call medium-term fault-tolerant computers, capable of around a trillion logical operations, a level known as the teraquop regime. They set the fusion and photochemistry results against application-scale machines roughly a thousand times bigger, a class that John Preskill has called FASQ, for fault-tolerant application-scale quantum computers. All three need far more than the million or so operations expected of the first fault-tolerant processors, and closing that gap will take further cuts of orders of magnitude. Google has set out its own path to useful applications, and recent work on error-correction models is part of the hardware side of that effort.
The spacetime measure also assumes the planar surface code, an error-correction scheme that arranges physical qubits on a flat grid where neighbours constantly check one another so errors can be spotted and repaired. The authors expect early machines to be shorter of qubits than of gates, which would argue for weighting the two differently.
The proofs behind Lean quantum algorithms also have limits that are easy to miss. Lean shows that a circuit meets its formal specification and its cost claim, and it does not show that the specification matches nature. The agents can only optimise what they are asked to, and the authors point to two places where the specification held them back. To match its baseline, the photochemistry file demands correct behaviour even on states a real molecule could never be in. The cytochrome P450 file locks in one way of factorising the energy expression, which rules out the kind of change in representation behind several recent advances by human researchers. The paper does not claim that classical computers cannot do these simulations either, because every comparison is against an earlier quantum design.
The authors expect people to spend more of their time writing faithful specifications and interpreting what comes back. They also want to extend the specifications to cover error correction and the physical layout of qubits on a chip, so that algorithms and hardware can be tuned together. The Lean library, the problem files and the verified solutions are due to be released as open source shortly. Until then nobody outside the team can check the proofs, and every cost figure in the paper is, for now, the authors’ claim.
Where theorem proving and quantum computing go next
Theorem provers come in two broad families. Interactive theorem proving, or ITP, means a person steers a proof assistant such as Lean, Rocq or Isabelle, writing each step and letting the machine check it. Automated theorem proving, or ATP, means a program searches for the proof on its own, as SMT solvers and other automated provers have long done for narrow problems.
The two have been converging for years, and the Lean code in this article shows it. The grind tactic in the screenshots above borrows the reasoning of SMT solvers, so that a single word closes a proof a person once wrote out by hand. The paper pushes the same idea much further. A human writes the specification and an agent searches for the program and the proofs that fill each sorry. Lean’s small kernel then checks the result, which makes the agent an automated prover working inside an interactive one.
If that pattern holds, the likely trend is a division of labour in which people write and audit specifications, machines do the searching, and the kernel stays small and trusted. The hard problem moves from finding proofs to asking the right question, which the authors acknowledge when they expect researchers to spend more of their time writing faithful specifications. A proof can only be as good as the statement it proves, and the agents that gamed a scoring rule in this paper show why that matters.
Quantum computing may be the field where this matters most, because it is the one where testing runs out first. Nobody can run an algorithm on thousands of logical qubits on a laptop to see whether it works, and the hardware that could run it does not yet exist. A proof is the best evidence available before the machine is built. The authors want to extend their specifications to cover error correction and the physical layout of qubits, so that algorithms and hardware can be proved against each other.
There is a neat fit with the name on the lab’s door. Google Quantum AI has built hardware such as the Willow chip, and this paper is an unusually literal case of both halves of that name at work. The AI half designs the algorithms and the proof checker certifies them, while the quantum half is the machine that will one day run them.
None of that is settled. The Lean library and the proofs are not yet public, and the circuits are far from any real machine. Agents that can search a great many candidate circuits can also search for ways to fool a scorer. What the paper shows is a way to design Lean quantum algorithms, a method suited to a field whose machines nobody can yet switch on. If quantum computers arrive, the programs they run may be written by one kind of machine, proved by a second and executed by a third, and the first two are already working together.
See today’s quantum computing news on Quantum Zeitgeist for the latest breakthroughs in qubits, hardware, algorithms, and industry deals.
