what i got to know from wikipedia is as follows m not talking about this group here:-
Metamath is a language for developing strictly formalized mathematical definitions and proofs[1] accompanied by a proof checker for this language and a growing[2] database of thousands of proved theorems covering conventional results in logic, set theory, number theory, group theory, algebra, analysis, and topology, as well as topics in Hilbert spaces and quantum logic.