Does a (public) database of theorems exist, as integer sequences are cataloged in the Online Encyclopedia of Integer Sequences (OEIS)?
$\endgroup$ 22 Answers
$\begingroup$The Metamath Proof Explorer "... has over 12,000 completely worked out proofs ..." [1] accessible via an indexed theorem list. [2] Each theorem has a corresponding unique label.
The main Metamath page describes the project, the Metamath language, and programs and databases available for use. [3] The Metamath proofs are mechanical, and may or may not be useful because of their tedium and lack of insight.
An alternative to Metamath is Ghilbert [4], which looks much nicer. For example, contrast the Ghilbert proof of Euclid's Theorem [5] with the Metamath proof of infinitely many primes. [6] Unfortunately, Ghilbert does not seem to have an indexed database of theorems like Metamath does.
Some ad hoc lists of theorems that do not include canonical identifiers are:
The Cut the Knot and Wolfram Mathworld web sites are worth mentioning, if only because they have extensive collections of mathematical resources, many theorems included.
The following is a list of some related answers on math.SE. However, these answers did not address a canonical indexing of the theorems.
- The most common theorems taught in Abstract Algebra
- Does anybody know of a site that has a set of all theorems?
References:
- [1]
- [2] (inline GIF images) and (unicode)
- [3]
- [4]
- [5]
- [6]
I might also add that ProofWiki is a community project to do such, complete with proofs.
$\endgroup$
