Metamath

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

參考資料
外部連結

• [http://us.metamath.org Metamath] : 官方網站

數學軟體
數理邏輯