Google's AI agents discover formally verified quantum algorithms in Lean

[StarKnight90]

AI is now helping to design quantum algorithms and prove they work. Quantum Computing Report covers a paper from Google DeepMind and Google Quantum AI, titled Discovering Formally Verified Quantum Programs with AI

Teams of Gemini based agents share lemmas and critiques through a shared wiki, using formal quantum Hoare logic. An independent Lean checker verifies the proofs and allows no custom axioms

Results are given as the peak logical qubit count multiplied by the T gate count. The biggest gain was over 290 times lower for 25 bit arcsin state preparation, with 10.9 times lower for fusion stopping power, 8.08 times for photochemistry and 2.49 times for cytochrome P450

Grover multi target search needed 1.22 to 2.55 times fewer rounds. The report notes that the order of magnitude framing overstates some results, there has been no hardware demonstration, and classical checking is not feasible at this scale, so the proofs are the only check

Using formal proofs to guarantee that quantum programs do what they claim is a clever way to build trust in AI generated work. Big reductions in resource costs could bring useful quantum chemistry closer. The lack of hardware testing means it is early days, but the method looks powerful

Should we trust AI designed algorithms if they come with formal proofs? And which applications would benefit most from these savings?

Google DeepMind and Google Quantum AI Use Lean 4 to Discover Formally Verified Quantum Algorithms - Quantum Computing Reportquantumcomputingreport.com