Mathematics source

Sources for mathematics, based on set.mm from Metamath language To create a head version of the base from set.mm do:

1. run metamath set.mm
2. in the metamath console type save proof * /normal
3. write uset.mm
4. exit

Caution: the size of the obtained source uset.mm file will exceed 150 mb.

Several smaller fragments of the whole metamath base are included into the repository:

• uset-10000 - the first 10 000 lines of uset.mm
• uset-50000 - the first 50 000 lines of uset.mm
• uset-100000 - the first 100 000 lines of uset.mm