Google teams use Gemini 4 and Lean to find formally verified quantum programs, claim up to 290× cost cuts

Researchers from Google DeepMind and Google Quantum AI say they have used Gemini 4-based AI agents and the Lean theorem prover to discover new quantum programs and formally verify that they can sharply cut estimated costs for several important quantum-computing tasks. In a paper posted to arXiv, the team reports improvements including more than 290 times lower cost for a fixed-point arcsin routine used in fault-tolerant arithmetic, along with smaller but still significant gains for parallel Grover search and chemistry and fusion-related simulations.

What makes the claim notable is not simply that AI helped design quantum algorithms. The paper argues the resulting programs come with machine-checked proofs of both correctness and resource cost, allowing researchers to assess algorithms that may be too large to test directly on current classical computers and far beyond what today’s quantum hardware can run. As the abstract puts it, “Combining human and artificial intelligence at scale, under the rigor of mathematical proof, lets researchers design algorithms that today’s classical and quantum computers cannot test, shortening the path to practical quantum computation.”

The paper, “Discovering formally verified quantum programs with AI,” was posted as arXiv:2611.09822. Version 1 appeared Nov. 6, 2026, version 2 on Nov. 9, and the PDF is dated Nov. 10. Authors include Google DeepMind researchers Sergey Shirobokov, Ben Jaderberg, Katerina Hristova and Pushmeet Kohli, and Google Quantum AI researchers including George Tsoukalas and Johannes Bausch.

The headline results are framed as formal improvements over published baselines under the paper’s specifications and cost models. For fault-tolerant arithmetic, the team reports a more than 290x reduction in Q·T cost for fixed-point arcsin. Q·T is the paper’s main resource measure, defined as logical qubits multiplied by T gates, a key count for fault-tolerant quantum computing.

For search, the paper reports up to 2.55x lower expected oracle rounds for parallel Grover search, a quantum search method often discussed as a building block for broader algorithms.

The paper also reports large reductions for physics and chemistry applications. In a fusion-related stopping-power simulation involving alpha particles and hydrogen, the researchers report a 10.9x lower Q·T cost. For a photochemistry benchmark based on non-Born-Oppenheimer molecular dynamics, they report an 8.08x lower Q·T cost. For a drug-metabolism application involving cytochrome P450 energy calculations, they report a 2.49x lower Q·T cost.

To produce those results, the researchers say they built a Lean library for quantum programs, including a quantum Hoare logic framework, so AI agents could generate candidate programs from formal specifications and produce machine-checked proofs of correctness and resource bounds. Lean is a theorem prover, software used to write proofs that can be checked by a computer. The paper says, “All large-scale experimental runs of autonomous discovery were performed using Gemini 4 Carbon models.”

The workflow described in the paper relies on multiple AI-agent teams, a shared version-controlled wiki of verified results and helper lemmas, and scheduled cross-team “conferences” to exchange ideas. The paper also describes a safeguard meant to limit false positives: submissions were accepted only after an independent external verifier replayed them in a clean sandbox against a frozen specification, checked that no placeholder proofs remained and confirmed that the cost theorem reduced to the claimed closed-form result.

The authors are explicit about what the work does and does not show. These are formal proofs under written specifications and cost models encoded in Lean, not demonstrations on quantum hardware. The paper also says many of the discovered circuits are too large to be classically simulated, which is why formal verification matters here. That also means the results depend on the correctness of the specifications and cost assumptions the team chose to formalize.

For now, outside researchers will have to wait for the underlying materials to judge how easily the work can be reproduced. Under code availability, the paper says, “Our Lean library will be open sourced shortly, together with the problem specifications and verified solutions discussed in this manuscript.” Until then, the claims remain those of an arXiv preprint — striking if they hold up, but still awaiting broader scrutiny through the promised code and proof release.