{"id":"arxiv/2610.30216","url":"https://arxiv.org/abs/2610.30216","tags":["quant-ph"],"score":0,"title":"Lean-QuantumAlg: A Framework for AI Agents to Produce Quantum Algorithms that Humans Can Trust","domain":"quant-ph","source":"arxiv","authors":["Lei Zhang","Mingrui Jing","Yusheng Zhao","Jiahong Liu","Xin Wang"],"reviews":0,"subject":"quant-ph","summary":"AI agents are increasingly capable of constructing quantum algorithms and proofs, yet machine-checked proofs alone cannot guarantee that the intended problem is solved or that resource claims match the verified computation.Here we introduce Lean-QuantumAlg, a Lean 4 framework for trustworthy AI-assisted development of quantum algorithms.Its Algorithm-Solves-Problem contract binds correctness, success probability, borrowed-state restoration and quantum and classical resource bounds to a single execution, while separating the guarantees that Lean checks from the problem specifications and…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-10-21","reactions":{}}