Prove-It is a tool for proving and organizing general theorems using Python. These web pages are a companion to the Prove-It code repository, generated using this code to display the proofs contained therein, in addition to the documentation. This system is in an early beta version and under active development. A tutorial and more complete explanation of Prove-It's unique approach to theorem proving is in progress.
Our proofs are organized into a hierarchy of contexts as listed below. This is an expanding and evolving library with the eventual aim of accepting proofs from many contributors. There is a particular structure to this library described in this brief guide. The links below go to corresponding context web pages. Each of these contains context-specific links to web pages for common expressions, axioms, and theorems, as well as a page of demonstrations containing relevant examples. Additionally, each generated expression links to an expression information page that shows the internal tree-like structure of the expression. Each theorem links to its proof, though not all proofs have been generated. This content is very much incomplete. The earlier contexts listed below tend to be more complete than the later ones. The proveit.logic.equality context has the best example of an ideal demonstrations page.
import proveit %contents packages/proveit