Metamath

Metamath
	File:Metamath logo.png
开发者	Norman Megill
当前版本	Template:Software version
源代码库	页面Template:Plainlist/styles.css没有内容。 {{URL\|example.com\|可选的显示文本}}; Module:EditAtWikidata第29行Lua错误：attempt to index field 'wikibase' (a nil value)
编程语言	ANSI C
引擎	页面Template:Plainlist/styles.css没有内容。 Module:EditAtWikidata第29行Lua错误：attempt to index field 'wikibase' (a nil value)
操作系统	Linux, Windows, Mac OS
类型	电脑补助证明验证
许可协议	GNU通用公共授权条款 (数据库使用创用CC)
网站	http://metamath.org

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

参考资料[编辑]

↑ Megill, Norman. What is Metamath?. Metamath Home Page. [2015-04-19]. （原始内容存档于2020-11-24）.
↑ Megill, Norman. Most recent proofs. Metamath Proof Explorer. [2015-04-19]. （原始内容存档于2020-02-03）.