  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.
