In a paper submitted on November 6, 2026, Google DeepMind and Google Quantum AI describe AI agents that design quantum programs. Such agents carry out multi-step tasks on their own. Working in teams, the agents found programs up to 290x cheaper than the best published designs, on a cost measure the researchers set. They also proved them correct in Lean, a proof assistant that accepts a proof only after checking every step.
The proofs stand in for tests: programs built for thousands of qubits are too large for an ordinary computer to simulate, and no quantum computer can run them yet.
The paper is on arXiv, the open archive where researchers post papers before peer review. Its 25 authors report 290x on a math subroutine and 10.9x on a simulation relevant to fusion research. The teams also shared a wiki and met at scheduled “conferences.” On three physics and chemistry problems, the authors trace about a quarter of the gains, on average, to those meetings.
From tested circuits to proved programs
On October 16, Anthropic reported that its Claude model designed quantum circuits up to 39x cheaper than the best published ones. In that study, an ordinary computer tested each circuit. The Google paper says AI testing has so far been “restricted to circuit regimes that can be classically simulated.”
The new work replaces testing with proof. Researchers first write a specification in Lean: a formal statement of what the program must compute, to what accuracy, and how its cost is counted. The agents then supply the program, its claimed cost and proofs of both. Lean flags every broken step, and the agents revise until the proofs pass.
For four of the five problems, cost equals logical qubits times T gates. Logical qubits are the error-corrected qubits a future machine would compute with. T gates are especially expensive operations on such hardware. The fifth problem counts query rounds instead.
How the agent teams worked
Each researcher chose “the agent framework, models, prompts, and division of labor.” Setups ranged from a single agent to hierarchical teams that split design, error analysis and proof writing. The paper does not name the language models behind the agents.
Because agents can edit any file in their workspace, the authors warn that they “may exploit loopholes by weakening theorem statements, altering definitions, or adding axioms.” Axioms are statements Lean accepts without proof. An external checker reruns every submission in a clean, isolated environment. The Lean Comparator, a checking tool, then confirms that the target theorems and definitions match the frozen specification.
Verified results go into a wiki shared by all teams: the best solution for each problem, reusable Lean files and notes on ideas that failed. As a rule, a new best solution must cut the cost by at least 5%.
Every four hours, teams also meet on a shared forum, the “conferences,” to question each other and propose new designs. Claims made there “carry no weight until independently verified and published to the wiki.”
Five problems, five gains
The first problem is parallel Grover search, a quantum method for finding marked items in a list with several queries at once. The verified programs need up to 1.22x fewer query rounds to find one item and up to 1.41x fewer to find all of them.
The 290x result is for arcsin, the inverse sine function, which quantum algorithms use to load numbers into a quantum state. The baseline, a 2018 design by Thomas Häner, Martin Roetteler and Krysta Svore, needs more than 440,000 T gates on 245 qubits. The agents’ circuit uses 3,698 T gates on 100 qubits.
The other three problems are scientific simulations. The first, relevant to fusion research, models how fast the fuel absorbs energy from alpha particles, the helium nuclei that fusion reactions release. It tracks one alpha particle and 218 electrons moving among 216 fixed protons.
The fusion baseline, a 2024 estimate by a team that included three of the new paper’s authors, needs 5,650 logical qubits. The new program needs 4,374 logical qubits and about 8x fewer T gates, for a cost 10.9x lower. Its main idea is to place the electrons on a spatial grid, where physics allows at most two per point.
The last two come from chemistry. One simulates the motion of a molecule of the kind studied for light-driven reactions, with all 47 nuclei and 187 electrons treated as quantum particles. The agents’ program is 8.08x cheaper.
The other computes energy levels of Compound I, a short-lived form of the cytochrome P450 enzymes that break down most medicines. The agents’ version is 2.49x cheaper and needs 333 logical qubits instead of 481.
How much the conferences added
The authors credit their best solutions to collaboration across teams. Seven teams worked on the molecule problem, and the best result changed hands seven times after the first run. The largest single drop, 34%, began as one team’s proposal at a conference. A second team refined and proved it.
Averaged over the three scientific problems, once the wiki and conferences were both running, 61% of the cost reduction came from ideas found inside a team. The wiki supplied 15% and the conferences 24%. The paper adds that credit “is often hard to separate cleanly.” Dead ends were shared too: a note proving why a proposed shortcut fails stopped two proposals from other teams.
Other recent work with Lean
Other groups are building similar tools. On October 13, Mingsheng Ying and colleagues published QEDIA, an open Lean library for checking quantum programs, built with an AI proof-writing agent under human supervision. The Google paper cites it as concurrent work.
On October 21, Lei Zhang and colleagues presented Lean-QuantumAlg, nine quantum algorithms that AI formalized, that is, wrote out as Lean proofs. They range up to quantum attacks on RSA-2048, a widely used encryption standard. The Google paper says such projects verify known algorithms, while its own system uses the proof to search for cheaper ones.
Lean has also spread beyond quantum computing. In October, the company Axiom Math used AI agents to turn a 15,000-page proof into Lean code in 24 days. On November 6, the startup PSI said an unreleased Anthropic model had proved an 18-year-old quantum conjecture, with 648 theorems checked in Lean.
On November 9, Anthropic said a team of 1,000 Claude Fable 5.2 agents formalized Fermat’s Last Theorem in 30 hours. The company’s first formalization, by an unreleased research version of Claude, had taken 11 days.
Limits the paper states
The three simulation programs remain far beyond near-term hardware. Many useful applications need from a billion to a quadrillion operations, the paper says. Early fault-tolerant processors, the first machines able to correct their own errors, are projected to handle about one million. The authors write that their simulations “still demand far more resources” than those machines, and that closing the gap “will require further orders-of-magnitude improvements.”
Most of the 290x came from classical testing. The agents first searched a restricted family of circuits that an ordinary computer can check in seconds, reaching a cost more than 200x below the baseline. Lean then pushed it further, and a last 11% cut came from circuits outside that family.
Two choices favor the arcsin baseline. It was built for an error near one in a million, looser than the task’s one in eight million. The authors also count only a lower bound of its cost. In the other direction, they note that a newer square-root circuit could cut the baseline’s cost by up to 3x.
Lean checks each proof against its specification, but people must judge whether the specification captures the physics. Agents found loopholes, such as “exploiting how Toffoli gates were counted without improving the circuit” (Toffoli gates are a standard three-qubit operation). Researchers and agent teams closed them by revising the specification. The cost measure also leaves out error-correcting codes, qubit routing and chip layout.
Humans kept the key decisions. Researchers chose the problems, wrote the specifications and picked their team setups. In the paper’s words, AI discovery backed by formal proof “shifts where human effort is applied.” The paper is a preprint, not peer reviewed, and its Lean library “will be open sourced shortly.”
What it means
For AI design of quantum algorithms, checking has been the bottleneck. Until now, AI search was limited to designs an ordinary computer can simulate, which rules out most programs for large machines. This paper shows agents searching programs for thousands of qubits, with a proof standing in for the missing test.
Every gain it reports is a cost proved on paper; nothing ran on a quantum computer. The paper presents such savings as one half of the path to useful machines, with hardware progress as the other. For researchers, the work shifts from deriving circuits by hand toward writing specifications tight enough that agents cannot game them.
The paper leaves two questions open: which models did the work, and how much computing it took. The next checkpoints are the release of the Lean library, with its specifications and solutions, and peer review of the paper. Outside groups can then rerun the proofs and test the specifications.
Sources
- Discovering formally verified quantum programs with AI, Sergey Shirobokov, Ben Jaderberg et al. (Google DeepMind, Google Quantum AI), arXiv, November 6, 2026
- Optimizing Quantum Circuits for Arithmetic, Thomas Häner, Martin Roetteler and Krysta Svore, arXiv, May 31, 2018
- Quantum computation of stopping power for inertial fusion target design, Nicholas C. Rubin et al., arXiv (published in PNAS in 2024), August 23, 2023
- comparator: A trustworthy judge for Lean proofs from untrusted sources, Lean FRO, GitHub, retrieved November 10, 2026
- QEDIA: Quantum Program Verification in Lean, Yuanjie Ren, Zhicheng Zhang, Junyi Liu, Jinzheng Li, Yidi Qi and Mingsheng Ying, arXiv, October 13, 2026
- Lean-QuantumAlg: A Framework for AI Agents to Produce Quantum Algorithms that Humans Can Trust, Lei Zhang, Mingrui Jing, Yusheng Zhao, Jiahong Liu and Xin Wang, arXiv, October 21, 2026
- Introducing Claude Fable 5.2 and Claude Mythos 5.2, Anthropic, November 9, 2026
Header image: chart by MACCUS, data from Shirobokov et al. (Google DeepMind, Google Quantum AI), arXiv 2611.09822, November 6, 2026
