  The general-purpose interactive theorem-proving assistant called Prove-It was
used to verify the Quantum Phase Estimation (QPE) algorithm, specifically
claims about its outcome probabilities. Prove-It is unique in its ability to
express sophisticated mathematical statements, including statements about
quantum circuits, integrated firmly within its formal theorem-proving
framework. We demonstrate our ability to follow a textbook proof to produce a
formally certified proof, highlighting useful automation features to fill in
obvious steps and make formal proving nearly as straightforward as informal
theorem proving. Finally, we make comparisons with formal theorem-proving in
other systems where similar claims about QPE have been proven.
