Are there any archives or databases of mathematical theorems in an
easily machine-parsable format (e.g. MathML or TeX, but NOT image
files) available free or at low cost to the public?

If any such exist, I am particularly interested in ones which also
carry proofs of theorems.

Any area of math will do, but I am particularly interested in
foundations (set theory, logic, etc.)

---

Request for Question Clarification by mathtalk-ga on 25 Dec 2002 07:42 PST

Hi, greenrd:

Thanks for posting this interesting question.  There are some formats
specific to theorem proving software.  Would archives of that nature
be of interest?

MathML has a sort of split personality, between presentation and
content, and TeX is all about presentation, IMHO.  If you are
interested in machine verifiable proofs, I suspect you'll be
interested in these other formats, too.

regards, mathtalk-ga

---

Clarification of Question by greenrd-ga on 25 Dec 2002 08:15 PST

Yes, I would be interested in other formats. I think you're right that
math in content-oriented formats is easier to process. (Note that
MathML can be used as a pure content format, although I don't know if
many people are using it that way yet.)

By the way, I just changed the price from $2 to $10, as I realised $2
looks a little Scrooge-like compared to most of the other questions!

Hi, greenrd-ga:

Thanks for changing the price; I couldn't in good conscience have
asked you to do it because the subject interests me so much, I already
prepared this answer!

regards, mathtalk-ga

The theorem proving system with which I am most familiar is Mizar,
started back in 1973 and remains very active:

[Mizar Home Page]
http://mizar.uwb.edu.pl/

The Mizar system is useful both as a theorem proof verification system
and as a formal software specification tool:

[MML (Mizar Mathematical Library)]
(contains over 2000 definitions and 30,000 theorems)
http://mizar.uwb.edu.pl/library/

[The QED Manifesto]
http://www.cs.kun.nl/~freek/qed/qed.html

There exists such a variety of approaches to automated theorem proving
that it is natural for some effort to be given to unification of these
platforms.  One such group effort (albeit not very active) is HELM:

[Hypertextual Electronic Library of Mathematics]
(closely associated with the COQ theorem proving system)
http://helm.cs.unibo.it/

which, like MathML, embraces XML as a "vehicle" for cross-platform
support and development of mathematical reasoning software.  A recent
discussion of the status of "porting" Mizar to XML formats can be
found here:

http://mizar.uwb.edu.pl/forum/archive/0207/msg00018.html

This effort aims at providing a common library of benchmark/test
problems:

[TPTP (Thousands of Problems for Theorem Provers) Problem Library]
(Also has links to similar collections of Automated Theorem Proving
problems)
http://www.cs.miami.edu/~tptp/

Additional Links of Interest:

[Automated theorem proving, From Wikipedia]
(Brief discussion)
http://www.wikipedia.org/wiki/Automated_theorem_proving

[Computer Algebra meets Automated Theorem Proving: Integrating Maple
and PVS]
(detailed discussion)
http://www.csl.sri.com/users/owre/papers/tphols01/tphols01.pdf


Search Strategy:

Keyword: mizar
://www.google.com/search?hl=en&ie=UTF-8&oe=UTF-8&q=mizar&btnG=Google+Search

Keywords: mizar XML
://www.google.com/search?hl=en&lr=&ie=UTF-8&oe=UTF-8&q=mizar+XML&btnG=Google+Search

Keywords: "theorem proving" automated
://www.google.com/search?hl=en&ie=UTF-8&oe=UTF-8&q=%22theorem+proving%22+automated&btnG=Google+Search

---

Clarification of Answer by mathtalk-ga on 26 Dec 2002 12:18 PST

greenrd-ga, thanks for the generous rating (and tip!).  If you need
any clarification to this answer, please ask!

-- mathtalk-ga

Great links, thanks

Hi greenrd, here are some more pointers:

From the way you ask the question, I think that you might be interested
in looking at the Metamath system.
http://metamath.org/

The HOL Light system by John Harrison has only about 3000 theorems, but
it is one of the most interesting systems for formal math that I know of.
http://www.cl.cam.ac.uk/users/jrh/hol-light/

According to Randy Pollack, the best system for formalizing mathematics
is the Isabelle system (which has a Mizar-like language called Isar).
It certainly has many aspects that make it very interesting.
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/

If you're interested in proof representation, there is the OMDoc encoding
(but not everything fits in it, and there is not a significant body of
OMDoc-encoded math yet).
http://www.mathweb.org/omdoc/

To see what a simple mathematical proof looks like in fifteen different
systems take a look at:
http://www.cs.kun.nl/~freek/comparison/comparison.ps.gz

Hi, wondering-ga:

Thanks for your interesting and very cogent comments/links.

In downloading the last link, I found that it (despite the .gz
extension) is an uncompressed PostScript file.  Simply renaming it
allows it to be opened with GhostView.

regards, mathtalk-ga