有這麼一個網站，已經存儲了26000多條定理。并且所有的定理的證明也都被存儲起來，通過了電腦驗證，這就是“Metamath”（https://us.metamath.org/）。
希爾伯特曾經這樣看待數學，他認為數學證明就是一個符号遊戲。一個數學證明中所有的符号即使替換成任何東西，推理仍然可以繼續，隻要我們确立對這些符号進行推理的規則。這種對數學的觀點，後來被稱為“形式主義”。
羅素和懷特海德的巨著《數學原理》就是對實施以上想法的一種嘗試。《數學原理》一書希望能從最基本的定義和公理開始，像字典般一步步推導出當時已知的所有數學。
（《數學原理》一書的封面）
但可想而知，這個工作量是巨大的。全書一共分為三卷，2000多頁，一共寫了10餘年。内容繁複細緻到令人發指，以緻于“1+1=2”到379頁才出現，而“2+2=4”則被歸在第二卷。
而現在，Metamath（https://us.metamath.org/）項目正在嘗試重新用形式化語言來存儲人類所知的數學内容。Metamath項目的工作原理很簡單：
把所有數學的定義、公理用符号存儲起來，這種符号形式被稱為“形式化語言”（Formal Language）。從定義和公理開始，如果一個新的命題中的所有元素可以按照“替換”規則，替換成已知的符号，那麼這個命題就是真命題，并且可以為新的命題所用。 比如，ZFC公理系統被編碼成：
（上圖：Metamath中，用形式化語言書寫的ZFC）
而皮亞諾算術公理中，“0是自然數”這句話，在Metamath中，是可以被證明的：
Metamath中，“0是自然數”的證明
證明用了三步，“ω”在這裡是有窮序數的意思。點選"Ref"一列下的連結，你可以看到每一個符号的來曆和這一步驟成立的依據。不能有無緣無故的符号，也不能有無緣無故的推導。 第三行中的“Hyp”一列，表示的是這一步驟的成立的前提，這裡表示最終結論需要用到第1、2行的兩個前提。而推理依據則是"ax-mp"。"ax-mp“是一條公理，系統中是這樣描述的：
ax-mp公理用人類“友好”的語言描述是這樣的：
Description: Rule of Modus Ponens. The postulated inference rule of propositional calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if is true, and implies , then must also be true". This rule is sometimes called "detachment", since it detaches the minor premise from the major premise. "Modus ponens" is short for "modus ponendo ponens", a Latin phrase that means "the mode that by affirming affirms" - remark in [Sanford] p. 39. This rule is similar to the rule of modus tollens mto189.
Note: In some web page displays such as the Statement List, the symbols "& " and "⇒ " informally indicate the relationship between the hypotheses and the assertion (conclusion), abbreviating the English words "and" and "implies". They are not part of the formal language. (Contributed by NM, 30-Sep-1992.)
Chatgpt的翻譯：
描述：Modus Ponens 規則。命題演算的公理化推理規則。請參見例如 [Hamilton] 第73頁的規則1。該規則表示，“如果 P 是真的，且 P 蘊含 Q，那麼 Q 也必須是真的”。這個規則有時被稱為“分離”，因為它将次要前提從主要前提中分離出來。"Modus ponens" 是 "modus ponendo ponens" 的縮寫，這是一個拉丁語短語，意思是“通過肯定而肯定的方式” - 見 [Sanford] 第39頁的評論。該規則類似于 modus tollens 規則 mto189。
注意：在某些網頁顯示中，如聲明清單，符号 "& " 和 "⇒ " 非正式地表示假設和斷言（結論）之間的關系，簡化了英語單詞 "and" 和 "implies"。它們不是正式語言（筆者注：這裡應該翻譯為“形式化語言”）的一部分。（由 NM 在 1992 年 9 月 30 日貢獻。）
而在Metamath中，證明是“簡單”的，基本隻有一個“等價替換”原則。以下是一個證明“2+2=4"的過程：
在step 1中，我們用Ref "df-2"定義了2，它就是“1+1”。
在step 2中，我們用到了“opreq2i”定理。這條定理說：
如果A=B，則CFA=CFB。
你問這裡的A、B、C、F是啥？完全不重要，可以是任何東西！重要的是，它告訴我們， A=B時，可以把它替換到其他等式中。如果我們認為“C”就是“2”，“F”就是“+”，“A”也是“2”，“B”是“1+1”，那麼由Step 1已知的條件和“opreq2i”定理，我們“推導”出了:
2+2=2+(1+1)
這就是形式化語言的推理，非常傻瓜，也非常冗長。但是，它有一系列的優點：
- 機器可以閱讀這樣的證明，因為機器隻要堅持替換工作是否正确即可。
- 每一步都有依據可循，可以確定證明無誤。
缺點也很明顯，要把一個命題的證明用形式化語言書寫出來太費勁了！關于根号2是無理數的證明用了94步之多！
（Metamath上，關于根号2是無理數的證明的最後幾步）
可想而知，其他證明要能正确書寫出來有多麻煩。
黑爾斯曾經為了確定其關于“開普勒猜想”的證明完全正确，啟動了一個叫FlysPecK的合作項目，把他的證明完全用形式語言重寫一遍。項目從2003年開始，到2014年結束，耗時11年之巨！
（Flyspeck項目中的形式化證明代碼）
盡管如此，Metamath中，已經存儲26000多條完整的數學定理的證明，目前還在不斷增加中。
你可能會問，為什麼不讓機器自動産生證明呢？不是不可能，但是困難還是非常大。
首先要把一個複雜命題寫成形式化語言就是一個非常繁複的過程。寫出來之後，怎麼有一個快速的算法，讓計算機去尋找證明，也是一個非常大的問題。如果隻是讓計算機暴力搜尋，試圖以已知的定理内容，去建立一條“路徑”，“連接配接”新的命題，這是非常困難的，目前沒有有效率的算法。
如果讓計算機自己“創造”新的命題，這倒是一條可行的思路。但問題也在于，如何把計算機創造出有“意義”翻譯成人類可以了解的語言，也是一件不容的事。另外，計算機也可能創造很多無意義的的命題，比如像“1000+1=1001”那樣。這樣的命題，計算機很“容易”發現，但是毫無價值。
關于Metamath的介紹就到這裡。總之，數學可以抽象成一種計算機語言，這種語言讓計算機閱讀很容易，但是對人來說就太困難了！