Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge

TL;DR

Prove-It is a Python-based interactive theorem prover with a user-friendly Jupyter notebook interface, designed to make formal proof construction as natural as informal reasoning, supporting complex mathematical and quantum applications.

Contribution

It introduces a flexible, expressive proof assistant that integrates with Jupyter notebooks, enabling easier formal theorem proving and documentation, with applications to quantum computing.

Findings

Successfully constructed a proof-by-contradiction for √2 not in Q

System avoids logical paradoxes like Russell's and Curry's

Supports future quantum computing applications

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 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.