Verifying quantum phase estimation using an expressive theorem-proving assistant
Wayne Witzel, Warren D. Craft, Robert D. Carr, Deepak Kapur
Abstract
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.