|back to jeremybem.org|
The Zermelo Proof Checker (ZPC) is a lightweight proof assistant based on standard set theory and Hindley-Milner type theory.
Obtaining and installing ZPC
Here is a proof that a Cauchy sequence of rational numbers is always bounded. If you save it as Example.zl in your home directory, the following command should succeed:
[~]$ zpc Example.zl [~]$
The result is an empty file called Example.czo. It has a timestamp and can be viewed as certificate that the proof was checked.