\abstract{ {\TeX} files are text files which are readable
by other programs. Mathematical proofs written
using {\TeX} can be checked by a Python program provided
they are expressed in a sufficiently strict
proof language. Such a language can be
constructed using only a few extensions beyond
the syntax of \cite{tb}, one being
the incorporation of explicit
theorem number references into the syntax.
Such a program has been applied to and successfully
checked the theorems in a significant initial
segment
of a book length mathematical manuscript.
}