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.
ProofCheck is based on syntactical ideas of
A. P. Morse.
We warn prospective
users that there is no magic to be found here. The unremarkable fact is
that doing complete proofs requires tedious citations of minutiae.
Experience to this point indicates that filling in the details
of proofs so that they become checkable increases their length by a factor
of two or three and the time required to write them by an order of magnitude.
Examples
To see examples of proofs which illustrate the
main features of ProofCheck
click on the following links:
Supporting Material
Downloads
Uploads
Proofcheck was written to check the proofs in a manuscript
in progress Foundations of the Topology of Manifolds
by Bob Neveln and
Bob Alps. This unfinished manuscript contains
hundreds of proofs. Currently over 500 of them check.
Other systems
are available. Most of these generate proofs rather than check
an author's text.
ProofCheck is described in a paper in
The PracTeX Journal.
and also in a talk
to a recent TeX Users Group conference.
If you have questions, suggestions, complaints, or a bug to report, please e-mail Bob Neveln and include "ProofCheck" in the subject header.