Quantum computers could solve important problems, but we need better quantum algorithms, step-by-step instructions for the computer. Finding those algorithms usually takes years of work by experts. The problem is that we cannot test quantum algorithms on real quantum computers yet, only on classical computers for tiny examples.
This research used AI agents to automatically discover new quantum algorithms. The agents worked in teams, sharing knowledge through a wiki and meetings. They wrote their candidate algorithms in the Lean theorem prover, a tool that mathematically proves the algorithm is correct and counts its resource use. An external verifier checked all submissions to prevent cheating.
The AI agents found better algorithms across several important tasks. The biggest improvement was a 290-fold reduction in the resources needed for a key quantum arithmetic operation. These results show that combining AI with formal mathematical proof can speed up quantum algorithm design, even for algorithms too large to test on today's computers.