Metamath

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

Metamath
Metamath logo.png
开发者Norman Megill
目前版本
  • 0.198 (2021年8月7日)[1]
编辑维基数据链接
源代码库 编辑维基数据链接
编程语言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). 

外部链接