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