DeepMind and Google Quantum AI report AI-discovered quantum programs verified in Lean

A team of 25 authors from Google DeepMind and Google Quantum AI, including Pushmeet Kohli, Ryan Babbush, Sergio Boixo and Swarat Chaudhuri, posted a preprint on arXiv describing a system in which teams of language-model agents propose quantum programs and prove them correct in the Lean theorem prover.

The paper starts from a stated problem: quantum algorithms can only be evaluated on classical computers for small or restricted instances, so automated discovery loops that work in mathematics and computer science are hard to trust here. The authors built a Lean library containing a classical-quantum programming language, a program logic for proving correctness, and resource counting that bounds quantities such as T-gate and qubit counts. Researchers write a problem specification as a Lean file with unfilled placeholders for the program, its cost bound and the proofs. Agent teams, which the paper says share results through wikis and “conferences”, fill them in, and Lean checks the result.

The abstract reports improvements on prior baselines for parallel search (up to 1.4 times), quantum arithmetic (290 times), and simulations relevant to fusion, photochemistry and drug metabolism (11 times, 8 times and 2.5 times respectively). These figures are the authors’ own, measured against the published baselines they chose, and the paper is an arXiv preprint; no peer review or outside assessment has been reported in the sources consulted.

What the Lean check establishes is narrower than the headline. It certifies that a program satisfies the specification a researcher wrote and that its stated cost bound holds; it does not show that the specification describes the physical problem the application cares about. The paper’s design leaves that step to the human authors of each specification. The abstract itself frames the programs as algorithms “that today’s classical and quantum computers cannot test”, so the claimed gains appear to be proven cost bounds in the Lean library rather than measured speed-ups on hardware.

The work belongs to a run of AI-generated results that come with Lean proofs, a pattern also seen in the exponential time hypothesis claims from OpenAI and Anthropic and in Axiom’s Stacks Project formalisation. It also follows Anthropic’s claim that Claude Mythos 5 improved on the best published quantum circuits, an earlier claim of improved quantum designs from an AI developer.