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
the 2012 Python conference.
As an
open system, its aim is to maximize user control.
Examples of Short Proofs
Supporting Material
Downloads (A New Version is Coming Soon)
If you have questions, suggestions, complaints, or a bug to report, please e-mail Bob Neveln and include "ProofCheck" in the subject header.