Does a (public) database of theorems exist, as integer sequences are cataloged in the Online Encyclopedia of Integer Sequences (OEIS)?
2026-03-26 04:30:24.1774499424
Is there a canonical database of theorems?
2.4k Views Asked by Bumbble Comm https://math.techqa.club/user/bumbble-comm/detail At
2
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.
References: