QEDIA is a new preprint describing a Lean 4 library for quantum programs that also contain classical variables. It formalizes a quantum Hoare logic, proves the logic sound for partial and total correctness, and applies it to examples including the quantum Fourier transform, phase estimation, repeat-until-success circuits and Hamiltonian simulation. The authors say an LLM-based prover agent helped build the library and program proofs under human supervision.
The real increment is architectural: verification has to connect quantum mechanics, a mixed classical/quantum program semantics, specifications and proof rules without letting one layer quietly disagree with another. That is a better test of an agent-assisted formalization pipeline than another isolated olympiad proof. It is still a preprint; the claim worth tracking is the open library and checkable artifact, not a broad victory declaration for autonomous mathematics. QEDIA preprint, posted Oct. 13