Metamath

Metamath是用来发展严格形式化数学定义及证明的一款语言^[2]，亦指用来验证该语言的证明验证器，以及存有逻辑、集合论、数论、群论、代数、数学分析、拓扑学、希尔伯特空间及量子逻辑^[3]等领域中数万条已证明定理且仍不断在增加中的数据库。

Metamath

开发者	Norman Megill
当前版本	0.198 (2021年8月7日)[1]
源代码库	github.com/metamath/metamath-exe
编程语言	ANSI C
操作系统	Linux, Windows, Mac OS
类型	电脑补助证明验证
许可协议	GNU通用公共授权条款 (数据库使用知识共享)
网站	http://metamath.org

参考资料

1. Release 0.198. 2021年8月8日 [2022年7月27日].
2. Megill, Norman. What is Metamath?. Metamath Home Page. [2015-04-19]. （原始内容存档于2020-11-24）.
3. Megill, Norman. Most recent proofs. Metamath Proof Explorer. [2015-04-19]. （原始内容存档于2020-02-03）.

外部链接

• Metamath （页面存档备份，存于互联网档案馆）: 官方网站