News
Gemini 4 Carbon Agents Find Lean-Verified Quantum Programs, One Reportedly Over 290x Cheaper
Researchers at Google DeepMind and Google Quantum AI describe teams of AI agents that design quantum programs in Lean and attach proofs of correctness and cost. For arcsine, the authors report a cost reduction of more than 290 times, though most of that came from classically checkable circuits, and against a newer baseline the gain could be closer to 100 times.
A team from Google DeepMind and Google Quantum AI has presented, in an arXiv preprint, a system in which AI agents design quantum programs themselves and prove them correct in the Lean proof assistant. The authors report that for one subroutine, arcsine, the resource cost fell by more than 290 times against a baseline. Most of that saving, however, came from classically checkable circuits, and the step verified only in Lean delivered the last 11 percent. The authors also note that against a newer baseline the gain could be closer to 100 times.
How the system works
The problem is that quantum algorithms can be checked on classical computers only for small or restricted instances. The preprint's authors write that they built a library of quantum programs in Lean, in which Gemini 4 agents write new programs against formal specifications and verify both correctness and cost.
According to The Quantum Insider, humans chose the problems, wrote the specifications and interpreted the results. When a proof failed, the error messages went back to the agents, which revised their work. A separate mechanism checked that the agents had not weakened a theorem, changed the task or added unsupported assumptions.
The agent teams shared results through a wiki and met at scheduled virtual conferences. Quantum Zeitgeist reports that the teams ran Gemini 4 Carbon models, some as single agents and some as hierarchies with separate roles for subroutine design, error analysis and proofs.
The numbers in the preprint
In the fusion-related simulation (stopping an alpha particle, with 218 electrons and 216 fixed protons), the number of logical qubits fell from 5,650 to 4,374 and the total cost dropped 10.9 times. In photochemistry (187 electrons, 47 nuclei, one femtosecond of evolution), the reduction was 8.08 times against a baseline that already included earlier improvements.
For Compound I of cytochrome P450, which matters for drug metabolism (63 electrons, 58 orbitals), the reduction is 2.49 times against an updated baseline. For parallel search, the authors' second preprint version reports an improvement of up to 2.55 times when finding all marked items and up to 1.22 times when finding any one of them. The first version said 1.41 times, and that is the figure The Quantum Insider cites.
The arXiv page notes that all improvements are measured against earlier baselines, not as absolute values.
The authors' caveats
The Quantum Insider stresses that the programs described still exceed what early error-corrected machines are expected to handle. Many applications require billions to quadrillions of logical operations, while projections for such machines point to around a million, so several more orders of magnitude of improvement are needed.
The method has limits too. Assigning credit among agent teams was sometimes difficult, and in photochemistry the requirement of correctness for every input state, including physically invalid ones, narrowed the room for optimization. In the P450 case the representation was fixed, which ruled out gains from changing it.
What comes next
The authors point to further directions: error-correcting codes, the movement of information between qubits, chip layout and cost measures tailored to hardware. For readers, it is a sign that AI agents are being paired with formal proof, though a proof only guarantees agreement with the specification. The Lean library is not yet public, so until it is released the cost figures remain the authors' claim.
