Does a (public) database of theorems exist, as integer sequences are cataloged in the Online Encyclopedia of Integer Sequences (OEIS)?

  • $\begingroup$ Wikipedia or Wolfram MathWorld are, somehow. $\endgroup$ – servabat Jan 20 '15 at 9:22
  • $\begingroup$ Wikipedia's List of theorems seems a good start. $\endgroup$ – Raymond Manzoni Jan 20 '15 at 9:57

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.



I might also add that ProofWiki is a community project to do such, complete with proofs.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.