Verifying Quantum Phase Estimation using Prove-It

We use Prove-It [arxiv:2012.10987, pyproveit.org], an interactive proof assistant for organizing and verifying mathematical knowledge, to formally prove the success probability guarantee of the quantum phase estimation (QPE) algorithm, closely following Nielsen & Chuang's (2000/2010) textbook presentation using similar notation.  The interactive proof construction flows naturally from an informal proof by automatically deducing simple steps (given prior development of dependent theory packages as well as some training in using Prove-It).  Our formal proof relies upon well-established mathematical theorems that are not themselves required to be proven in the system, which demonstrates a useful feature of Prove-It that enables proofs based upon conjecture. Prove-It also provides easily-navigable hyper-links to explore the dependency structure of the generated human-readable proofs while maintaining an easily-inspected list of axioms and conjectures used (directly and indirectly) in each proof.