Other databases

February 3, 2025 · View on GitHub

Here is a list of some other Metamath databases that we know of but are not included in this repository (sorted alphabetically by GitHub ID):

@david-a-wheeler's collection of test databases.
@digama0's Dependent-Type Theory.
@geohot's TwitchCoq has a few interesting 2+2 proofs.
@ishanpm's Linear Logic.
@jamesjer's Unlimited Register Machine and Hilbert Geometry is a fork of set.mm with very interesting work which has not been merged back.
@naipmoro's Laws of Form.
@pbrosnan's Number Theory Game based on peano.mm, with additions.
@rod-lin's Matching Logic - the result of a Kore-to-MM conversion.
@sctfn's older version of New Foundations (this has since been moved into this repository).
@sorear's A variation on Peano, whose goal is to treat Peano arithmetic as a first-order theory with terms.
@tirix's FOL without overloading.
@tirix's Q0 Logic.
@openai's MiniF2F is a collection of exercise statements from math olympiads. An updated fork is available at facebookresearch/MiniF2F.
@MostAwesomeDude's Jbobau is a formalization of the Lojban langauge.

Anyone can create a Metamath database, but we thought linking to some of them might be of use.