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. Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps using LaTeX.
Prove-It is a theorem-proving assistant that is designed with flexibility and expressivity in mind. As such, it can be used to reason about complex structures such as quantum circuits. We are currently developing the Prove-It library to prove correctness of quantum circuit manipulations during e.g., compilation.
For details see
“Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge” Wayne M. Witzel, Warren D. Craft, Robert D. Carr, Joaquín E. Madrid Larrañaga. arXiv:2012.10987.
and
“Proving Quantum Equivalences Using ProveIt, A Python Based Theorem Prover” J. E. Madrid Larrañaga and W. M. Witzel. Computer Science Research Institute Summer 2020 Proceedings, p. 215.