{"id":"arxiv/2610.17708","url":"https://arxiv.org/abs/2610.17708","tags":["quant-ph","cs.PL"],"score":0,"title":"QEDIA: Quantum Program Verification in Lean","domain":"quant-ph","source":"arxiv","authors":["Yuanjie","Ren","Zhicheng Zhang","Junyi Liu","Jinzheng Li","Yidi Qi","Mingsheng Ying"],"reviews":0,"subject":"quant-ph","summary":"Practical quantum programs interleave quantum and classical computation: classical data shape the quantum operations that are performed, and measurement outcomes shape the classical computation that follows. Formal verification of such programs in a proof assistant requires mechanizing a program logic that handles this interplay consistently at every level, from the mathematics of quantum mechanics, through program syntax and semantics, to specifications and proof rules. Such mechanizations, along with the program proofs built on them, typically require substantial manual effort. We present…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-10-13","reactions":{}}