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

Mizar has its own language. Here is a dictionary of a few of the basic expressions.## Isabelle

Isabelle has its own language:*Isar*. Here is a sample proof.## Coq

Coq has its own language. Here is a page from the manual.## HOL Light

HOL is an extension of the CAML language. Here is a sample of its documentation.