Is there a canonical database of theorems?
Does a (public) database of theorems exist, as integer sequences are cataloged in the Online Encyclopedia of Integer Sequences (OEIS)?
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:
- https://en.wikipedia.org/wiki/List_of_theorems
- https://en.wikipedia.org/wiki/List_of_mathematical_proofs
- http://www.regentsprep.org/Regents/math/geometry/GPB/theorems.htm
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] http://us.metamath.org/mpegif/mmset.html#overview
- [2] http://us.metamath.org/mpegif/mmtheorems.html (inline GIF images) and http://us.metamath.org/mpeuni/mmtheorems.html (unicode)
- [3] http://us.metamath.org/
- [4] http://ghilbert-app.appspot.com/
- [5] http://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/euclidthm
- [6] http://us.metamath.org/mpegif/mmtheorems99.html#mm9884s
I might also add that ProofWiki is a community project to do such, complete with proofs.