Metamath is a language for developing strictly formalized mathematical definitions and proofs accompanied by a proof checker for this language and a growing 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.
While the Metamath program (the associated language) is not accompanied with an aut...
More
Metamath is a language for developing strictly formalized mathematical definitions and proofs accompanied by a proof checker for this language and a growing 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.
While the Metamath program (the associated language) is not accompanied with an automated theorem prover, it can be regarded as important because the formal language behind it allows development of such a software; as of March, 2012, there is no "widely" known such software, so it still is not a subject of "automated theorem proving" (it can become such a subject), but it is a proof assistant.
While the large database of proved theorems follows conventional ZFC set theory, the Metamath language is a metalanguage, suitable for developing a wide variety of formal systems.
The set of symbols that can be used for constructing...
Less
