Open vs. Closed Systems
Mathematicians write proofs using in TeX; ProofCheck reads TeX. Mathematicians
use their own notation; ProofCheck learns it. Mathematicians refer to external
results; ProofCheck accepts these references. The user is not asked
to learn a new language. The following systems do.
To see this check any of the following links:
-
Mizar has its own language. Here is a
dictionary
of a few of the basic expressions.
- Isabelle has its own language: Isar . Here is a sample proof.
- Coq has its own language. Here is a page from the manual.
- HOL is an extension of the CAML language. Here is a sample of its documentation.
Freek Wiedjik's list is a rather exhaustive list of computer math projects
of all sorts.
Stormy Peters gives her views.