ProofCheck: Checking Proofs Written in TeX

Welcome to the web site that helps you to use TeX to write complete mathematical proofs that you can check with a Python script.

The basic structure of the checking program is very simple: each step of a proof to be checked is unified with one rule after another from a long list rules of inference, in search of a match. The step is checked if a match is found. A proof is checked if all its steps check.

ProofCheck is based on syntactical ideas of A. P. Morse. Its guiding philosophy is that complete formality is to be achieved using as little formalism and deviation from accepted mathematical notation as possible. ProofCheck is described in a paper in The PracTeX Journal, and in a poster presentation at a Python conference, PyCon2012.

As an open system, its aim is to maximize user control.

Examples of Short Proofs

Supporting Material

Downloads

If you have questions, suggestions, complaints, or a bug to report, please e-mail Bob Neveln and include "ProofCheck" in the subject header.