Metamath
Metamath是用来发展严格形式化数学定义及证明的一款语言[2]，亦指用来验证该语言的证明验证器，以及存有逻辑、集合论、数论、群论、代数、数学分析、拓扑学、希尔伯特空间及量子逻辑[3]等领域中数万条已证明定理且仍不断在增加中的数据库。
 | |
| 开发者 | Norman Megill |
|---|---|
| 目前版本 |
 |
| 源代码库 | |
| 编程语言 | ANSI C |
| 操作系统 | Linux, Windows, Mac OS |
| 类型 | 电脑补助证明验证 |
| 许可协议 | GNU通用公共授权条款 (数据库使用知识共享) |
| 网站 | http://metamath.org |
参考资料
- ^ Release 0.198. 2021年8月8日 [2022年7月27日].
- ^ 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）.