Researchers use Lean and LLMs to verify quantum programs

Researchers demonstrated the automated discovery of formally verified quantum programs using large language models and the Lean theorem prover. By collaborating in agent teams that synthesize and verify programs against formal specifications, the system achieved order-of-magnitude performance improvements on scientific applications including quantum arithmetic and chemical simulations. The approach enables the design of complex algorithms beyond the testing limits of current classical and quantum computers. Open article →