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.
Anyone can create a Metamath database, but we thought linking to some of them might be of use.