# 31. ProofCheck: Checking Mathematical Proofs written in TeX

- Type:
- Poster
- Audience level:
- Novice
- Category:
- Science

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

### Description

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.

### Abstract

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.