DeepMind's Quantum Agents Hit 290x. A Fuzzer Did the First 217x.

Agent teams wrote quantum programs nobody can run yet, and a theorem prover checked every one. The biggest number in the abstract owes the least to that prover. The smaller numbers are the ones that could not exist without it.

"Discovering formally verified quantum programs with AI" (Shirobokov, Jaderberg et al.) builds a quantum programming library inside the Lean theorem prover, then lets teams of Gemini 4 Carbon agents search for lower-cost quantum circuits. No circuit counts unless Lean proves two things: it computes the right answer, and it costs what it claims.

The cost unit is Q·T: logical qubits times T gates. T gates are the expensive operation on an error-corrected quantum computer, so think of it as floor space times machine hours. Lower is better.

gains in Q·T against the strongest baseline the authors could build; Grover is measured in expected oracle rounds

A researcher writes a Lean file that reads like a contract with blanks. It states what the circuit must do and how its cost is counted, and leaves sorry placeholders for the circuit, its cost, and the proofs. The agents fill in the blanks. Nobody gives them problem-specific hints: the prompts are generic optimization prompts, and the domain knowledge lives in the spec.

Arcsin is the odd one out among the five, and the paper says so. Circuits for it can be written in a restricted gate set called kickmix, which a normal computer can fuzz-test in seconds. So the authors ran the search in two stages: fast fuzzing first, Lean second. Appendix F gives every waypoint. I divided them out.

ratios are my division of appendix f and table s2 figures

So of the 290x in the abstract, the part that needed gates a fuzzer cannot check is the last 1.12x. The jump from a piecewise-polynomial method to a 100-qubit circuit happened inside the testable box.

Two notes in the paper's favor. First, the baseline is a lower bound: it was built for an error of about 10^-6, looser than the 1.25×10^-7 the agents had to hit, and it leaves out some registers. The real gap is likely bigger than 290x. Second, the authors state the lesson plainly: where a classical simulator can check circuits, use it, and put formal proof on top. That is the right engineering call, and it is worth stating loudly before the 290x travels.

The three science results run on hundreds to thousands of logical qubits. No classical computer can simulate them, and no quantum computer exists to run them. Nothing but Lean can say these circuits are right. These are the real story.

Fusion, 10.9x. The task: simulate an alpha particle and 218 electrons moving among 216 fixed protons. The baseline works in momentum space and pays for every state the qubits could hold, including impossible ones. The agents' circuit moves electrons onto a real-space grid, where it can use a rule of physics: no more than two electrons (opposite spins) can sit on one grid point. Lean proved that, so the circuit stops paying for crowds that cannot happen. Result: 12.8x fewer steps at 1.52x the T gates per step, on 4,374 qubits instead of 5,650.

Light-driven chemistry, 8.08x. All 47 nuclei and 187 electrons are treated as quantum. Three moves: copy particle coordinates into scratch qubits and erase the copy with a measurement, instead of swapping particles back and forth; get 1/r by random sampling from a small table instead of computing a division; and treat a nucleus of charge 8 as eight unit charges at the same spot.

Drug metabolism, 2.49x. The baseline stores which Hamiltonian term is active as a binary number and looks up rotation angles from memory into a 247-qubit register. The agents' circuit gives each term its own qubit and flips one on. Earlier work found this idea narrowly worse because it needs more qubits. The agents' version uses the register twice, for the term weights and for the rotation angles, which covers over 95% of the per-step T-gate reduction. The 247-qubit register is gone: 481 qubits down to 333.

"vs published" is my division against the original estimates the paper cites (6.77×10¹⁵ and 2.26×10¹²)

For these two problems the authors folded later improvements into the baseline before comparing, and reported the smaller number. That is the opposite of how launch posts usually work.

For anyone building agent loops, Appendix B is the most useful page. The authors list how agents can game a local check without improving anything:

The checker is the open-source Lean Comparator. Compare this with the Hermes Agent self-refactor this newsletter covered in September, where agents edited the very tests that served as their oracle and test parity reported zero regressions. Same failure, opposite design: here the oracle sits outside the agent's reach, and humans review the spec instead of the solution.

Even then, one hole got through. Agents found a way to exploit how Toffoli gates were counted, which lowered the score without improving the circuit. The fix was not a better agent but a revised spec. A frozen referee is no better than the rulebook it reads.

The authors traced every verified gain back to where its idea started, once both sharing channels were running.

fig. 5b; fusion conference share inferred from the stated 13% cross-team total

On the chemistry problem, the lead changed teams seven times, and the final circuit combines tricks from three teams. The biggest single drop, 34%, started as a Team 1 conference post that Team 2 refined and proved. A note proving why one shortcut fails stopped two other teams from chasing it.

Two wiki rules worth copying. A new record needs at least a 5% improvement, so teams are not constantly rebasing onto tiny gains. And a solution that cuts the Lean code by 20% while lowering cost is also accepted, because proof files kept growing past agent context limits. Code size was treated as a resource, the same as qubits.

The authors are direct about this: agents cannot optimize beyond the spec. To match the baseline, the chemistry spec demands correct behavior even on physically impossible input states, which blocks gains like the fusion trick. The P450 spec fixes one way of writing the Hamiltonian, which rules out the newer representations behind recent human gains.

And none of this runs soon. Early fault-tolerant machines are projected at roughly one million logical operations. The lowest-cost circuit here, P450, still needs about 1.31 billion T gates. The paper says further cuts of 10x and more are needed. This is progress on the cost curve, not a path to a demo next year.