A team of researchers has demonstrated the automated synthesis of quantum programs using large language model agents, achieving improvements of up to an order of magnitude in scientific applications. The work addresses a well-known bottleneck: quantum algorithms can only be evaluated classically on small or restricted instances, which limits the automated discovery loops that already work in mathematics and computer science. The new platform makes it possible to design and validate programs without running them on classical simulators.

The method relies on a quantum program library built inside the Lean theorem prover. Agents synthesize novel programs from formal problem specifications and verify both their correctness and their cost, under the rigor of mathematical proof. Agents work in teams, share results and knowledge through wikis, and discuss ideas at organized conferences, mimicking the dynamics of a human research community.

The results improve on prior baselines for parallel search (up to 1.4x), quantum arithmetic (290x), and simulations relevant to fusion, photochemistry and drug metabolism, by factors of 11x, 8x and 2.5x respectively. 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.