
back to jeremybem.org 
The Zermelo Proof Checker (ZPC) is a lightweight proof assistant based on standard set theory and HindleyMilner type theory. Obtaining and installing ZPC
ExampleHere 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. 