Metamath
維基百科,自由的 encyclopedia
Metamath是用來發展嚴格形式化數學定義及證明的一款語言[2],亦指用來驗證該語言的證明驗證器,以及存有邏輯、集合論、數論、群論、代數、數學分析、拓撲學、希爾伯特空間及量子邏輯[3]等領域中數萬條已證明定理且仍不斷在增加中的資料庫。
Metamath是用來發展嚴格形式化數學定義及證明的一款語言[2],亦指用來驗證該語言的證明驗證器,以及存有邏輯、集合論、數論、群論、代數、數學分析、拓撲學、希爾伯特空間及量子邏輯[3]等領域中數萬條已證明定理且仍不斷在增加中的資料庫。