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.

翻译：通用交互式定理证明辅助工具Prove-It被用于验证量子相位估计算法，特别是其输出概率的相关论断。Prove-IT的独特之处在于其能够表达复杂的数学陈述，包括关于量子电路的表述，并紧密集成在其形式定理证明框架中。我们展示了遵循教科书式证明生成形式化认证证明的能力，重点介绍了通过自动化功能填补显而易见步骤，使形式化证明近乎与直观的非形式化证明同样便捷。最后，我们与其他系统中已完成类似QPE论断形式化证明的系统进行了比较。