Metamath

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

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

参考数据
  1. . 2021年8月8日 [2022年7月27日].
  2. Megill, Norman. . Metamath Home Page. [2015-04-19]. （原始内容存档于2020-11-24）.
  3. Megill, Norman. . Metamath Proof Explorer. [2015-04-19]. （原始内容存档于2020-02-03）.

外部链接
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.