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:

Freek Wiedjik's List

Freek Wiedjik's list is a rather exhaustive list of computer math projects of all sorts.

What is an Open System?

Stormy Peters gives her views.