Showing 1–2 of 2 results for author: Craft, W D
-
Verifying Quantum Phase Estimation (QPE) using Prove-It
Authors:
Wayne M. Witzel,
Warren D. Craft,
Robert 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 o…
▽ More
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.
△ Less
Submitted 4 April, 2023;
originally announced April 2023.
-
Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge
Authors:
Wayne M. Witzel,
Warren D. Craft,
Robert D. Carr,
Joaquín E. Madrid Larrañaga
Abstract:
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps using LaTeX. We review Prove-It's highly expressive representati…
▽ More
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps using LaTeX. We review Prove-It's highly expressive representation of expressions, judgments, theorems, and proofs; demonstrate the system by constructing a traditional proof-by-contradiction that $\sqrt{2}\notin\mathbb{Q}$; and discuss how the system avoids inconsistencies such as Russell's and Curry's paradoxes. Extensive documentation is provided in the appendices about core elements of the system. Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.
△ Less
Submitted 26 December, 2020; v1 submitted 20 December, 2020;
originally announced December 2020.
