跳至內容

Metamath

維基百科,自由的百科全書
Metamath
開發者Norman Megill
當前版本
  • 0.198(2021年8月7日)[1]
編輯維基數據鏈接
源代碼庫 編輯維基數據鏈接
編程語言ANSI C
操作系統Linux, Windows, Mac OS
類型電腦補助證明驗證
許可協議GNU通用公共授權條款 (資料庫使用創用CC)
網站http://metamath.org

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

參考資料

[編輯]
  1. ^ Release 0.198. 2021年8月8日 [2022年7月27日]. 
  2. ^ Megill, Norman. What is Metamath?. Metamath Home Page. [2015-04-19]. (原始內容存檔於2020-11-24). 
  3. ^ Megill, Norman. Most recent proofs. Metamath Proof Explorer. [2015-04-19]. (原始內容存檔於2020-02-03). 

外部連結

[編輯]