Skip to main content

For questions specific to the proof assistant Metamath. Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program.

For questions specific to the proof assistant Metamath. Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program. Its main library is set.mm using ZFC as its foundation.

References:
Known Metamath proof verifiers