31. ProofCheck: Checking Mathematical Proofs written in TeX

Audience level:
March 11th 8:30 a.m. – 8:35 a.m.


ProofCheck is a set of Python scripts which parse and check mathematics written using TeX. Its homepage is www.proofcheck.org. Unlike computer proof assistants which require immersion in the equivalent of a programming language, ProofCheck attempts to handle mathematical language formalized according to the author's preferences as much as possible.


ProofCheck is a suite of Python scripts that aid an author using TeX, parse and check mathematical proofs. The checking program is essentially a classic rule-based program where in this case the rules are logical rules of inference.

The presentation consists of:

I. An introduction itemizing the various scripts and their functions: parsing, checking, renumbering, etc. II A data-flow diagram showing the external supporting files needed: the rules of inference file, a common notions file, etc. III. A description of the Proof markup syntax needed to enable checking. IV. A sample proof (of the fact that divisibility is transitive) showing both the TeX source file and the PDF output file. V. A comparison of ProofCheck with well-known programs such as Mizar and HOL.