有这么一个网站，已经存储了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的介绍就到这里。总之，数学可以抽象成一种计算机语言，这种语言让计算机阅读很容易，但是对人来说就太困难了！