Google researchers use AI and proofs to cut quantum programs’ resource needs

Google DeepMind and Google Quantum AI researchers have used AI agents and mathematical proofs to design less resource-hungry quantum programs. Their study reports roughly elevenfold savings for a fusion calculation, with smaller gains in chemistry. The catch: even the improved scientific programs remain beyond the capabilities projected for early fault-tolerant quantum computers.

The preprint, Discovering formally verified quantum programs with AI, was submitted to arXiv on November 6, 2026, and revised on November 9. It describes Gemini 4 agents generating programs whose correctness and resource costs are checked mathematically.

The work tackles an awkward development problem. Researchers want quantum algorithms for calculations too large for ordinary computers to simulate, but suitable quantum hardware does not yet exist. Testing proposed improvements through conventional simulation therefore limits which programs can be explored. The team instead used proofs to check whether a program meets its requirements without reproducing its full quantum behavior.

Researchers built a quantum programming library in Lean, software that checks mathematical proofs. Humans selected the problems and specified the required calculation, accuracy and resource accounting. Agents then searched for solutions, supplying proofs of both correctness and cost. Failed proofs returned error messages that could guide another attempt.

A separate checker tested whether submissions still satisfied the original requirements. That safeguard was designed to stop an agent from claiming progress by changing the task, weakening a theorem or adding unsupported assumptions. Human researchers also interpreted the results; the agents did not define the scientific goals themselves.

Teams shared results through wikis and organized conferences. In the photochemistry task, one team proposed an idea at a conference and another refined and proved it. That exchange produced a 34% reduction—the largest single improvement in that program’s development sequence, according to The Quantum Insider’s account of the study.

For arithmetic and scientific calculations, the cost measure multiplies logical qubits by T gates. Logical qubits protect quantum information through error correction; T gates are operations that are expensive on error-corrected machines. The savings describe that combined resource measure, rather than execution times measured on a working quantum computer.

The fusion program studies how fuel absorbs energy from a passing particle. Its logical-qubit requirement fell from 5,650 to 4,374. Changes included a different representation of particle interactions and retaining electron-momentum information between steps, so the program did not have to calculate it again as often.

The photochemistry program tracks electrons and nuclei together over a brief period of molecular evolution. The drug-metabolism task instead estimates energy levels for a model of Compound I, a reactive form of cytochrome P450 enzymes. Much of its saving came from changing how information used to rotate electronic orbitals was stored and retrieved.

The researchers say several more orders of magnitude of improvement are needed to reach early fault-tolerant machines. Their specifications also limit the search in concrete ways:

• Photochemistry required correctness even for input states that would not describe physically valid particle arrangements, matching the baseline but constraining optimization.
• The P450 task fixed the mathematical representation of the molecule, excluding gains that might come from changing that representation.

Future specifications could include error-correcting codes, movement of information between qubits and physical chip layouts. Different machines may also favor different cost measures. The team plans to release its Lean library, problem specifications and verified solutions as open-source resources, allowing further work on the programs and the constraints used to judge them.