# PyProveIt/Prove-It

A tool for proving and organizing general theorems using Python.
Switch branches/tags
Nothing to show
Latest commit 529b304 Dec 7, 2018
Type Name Latest commit message Commit time
Failed to load latest commit information.
packages Dec 7, 2018
tutorial Dec 4, 2018
.gitignore Nov 7, 2018
COPYING Feb 2, 2017
build.py Dec 2, 2018
proveit_html.tpl Nov 26, 2018
setup.py Jan 15, 2017
tar_pvit_command.txt Dec 4, 2018

Welcome to Prove-It!

Prove-It is a tool for proving and organizing general theorems using Python.

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, hypothetical reasoning,
specialization, 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.

******************************************************************************************
Installation instructions

1) Make sure you have the required packages installed:
- Python2.7
- Jupyter

2) Run:

python setup.py develop

to install a link to the source tree in your python path, so that changes you make to
the code are immediately updated when Prove-It is imported.  This is recommended if
Alternatively, run:

python setup.py install

if you wish to install Prove-It into your main python distribution without
doing any development on the proveit packages.

3) Take a look at the "tutorial" folder.  It has numbered Juptyer notebooks
(and html versions for convenience) that introduce Prove-It concepts
in an appropriate order.  There are also tutorial notebooks/html in various
packages with specific information about that package.  A particularly
useful one is "proveit/logic/equality/equality_tutorial.ipynb" in the
"packages" folder.  Furthermore, there are "_proofs_" folders in various
packages with Jupyter notebooks that prove theorems of the package.  You
can peek at these for examples of how Prove-It works in practice.  Note that
"proofs" folders, without the underscores, are outdated proofs that will
likely fail to execute.

4) It is intended that packages continue to be added and updated to cover
an ever-expanding range of mathematical knowledge.  Packages may have
cross dependencies (as long as there is no circular reasoning in any
particular proof).  Classes/objects that should be accessible externally
should be imported in the __init__.py of the top-level package, and they
should be accessed, externally, at this top level.  For example, the
"Or" class is contained in "proveit.logic.boolean.disjunction.or_op.py" but
it can and should be accessed via "from proveit.logic import Or".
In this way, the sub-package structure can be useful for organization
purposes without being cumbersome to the user.  Here is the current list
of top-level packages under development, with brief descriptions:

_core_: Core Prove-It constructs required used to construct/verify proofs.
_generic_: Generic operations constructs (e.g., associative operations).
lambda_map: Useful methods/classes for generating Lambda maps
(e.g., compositions and sub-expression replacements)
logic: Boolean arithmetic, equality, and set theory.
number: Arithmetic and number theory concepts.
trigonometry: A few things pertaining to trigonometry.
linalg: A few things pertaining to linear algebra.
statistics: A few things pertaining to statistics.
physics: Currently just things related to proving the correctness of the
Quantum Phase Estimation algorithm at an abstract level.

******************************************************************************************
Version history

12 Feb. 2017
- Moved repository to github.com/PyProveIt/Prove-It.
12 Jan. 2017 - v0.3
- The code is now hosted on gitlab-ex.sandia.gov to make it accessible to
collaborators.
******************************************************************************************