Prove-It

Prove-It uses a powerful yet simple approach to theorem-proving. It is not designed with automation as the primary goal. The primary goal is flexibility in order to be able to follow, ideally, any valid and complete (indivisible) chain of reasoning. To that end, users can write additional Python scripts to make their own mathematical operations and LaTeX formatting rules. Axioms are statements that are taken to be true without proof. They can be added by the user at will in order to define their new mathematical objects and operations. Users can also add theorems that are to be proven. Theorems may be proven in any order.  Theorem proofs are constructed in Jupyter notebooks (interactive Python sessions in a web browser). These notebooks render LaTeX-formatted mathematical expressions inline. Proofs are constructed by invoking axioms and other theorems and employing fundamental derivation steps (modus ponens, deduction, instantiation, generalization, or axiom elimination).  Axioms and theorems may be invoked indirectly via convenience methods or automation (methods that are automatically invoked when attempting to prove something or as side-effects when something is proven). Theorem proofs and their axiom/theorem dependencies are stored in a kind of database (filesystem based). This database is used to prevent circular logic. It also allows users to track axioms and unproven theorems required by any particular proof. Convenience methods and automation tools may be added which utilize new theorems and aid future proofs. Mathematical objects and operations, axioms, and theorems are organized into built-in and user-defined packages.