最近几十年，基础性科学研究越来越受到世界范围的高度重视，形式化数学(formalized mathematics)和证明工程(proof engineering) 就是其中的一个重要研究方向。

形式化数学是一个有着超过30 年历史的基础科学研究领域，其总体目标是用计算机对数学理论进行形式化描述，对数学证明进行验证和检查，并且建立一个包含数学定义、定理和证明的形式化数学库。权威数学杂志Notices of the American Mathematical Society上有文章认为，形式化数学是第三次数学革命。2016.9封面

形式化数学的核心内容包括三部分：

1. 逻辑语言：一个能够描述数学知识的逻辑系统；

2. 证明工具：基于逻辑语言的证明工具；

3. 形式化数学库：通过证明工具验证的数学定理和数学证明所构成的数学知识库。

人类有史以来创造了极其丰富的数学理论，因此，形式化数学是一项巨大的工程。

形式化数学的技术和方法可以应用到软件和硬件的设计验证中。在形式化数学库的基础上，开发不同领域的形式化知识库，将促进信息科学在各个领域的发展。

形式化数学对数学发展的影响

维迪克(Wiedijk)[1] 认为，数学历史上发生过三次革命。第一次是公元前3 世纪，古希腊数学家欧几里得《几何原本》引入数学证明方法；第二次是19 世纪柯西等人引入“严格”数学方法，以及后来的数理逻辑和集合论；第三次就是当前正在进行的形式化数学。

形式化数学对数学的影响有两个方面：第一，检查数学证明的正确性；第二，促进数学基础的研究。

不久前，华人数学家张益唐在数学方面做出了接近菲尔兹奖水平的重大贡献，但是张益唐自博士毕业之后有几十年的时间找不到一份数学专业方面的工作，原因是他的博士论文引用了他的导师论文中的一个重要结论，而这个结论后来被发现是错的。

事实上，公开发表的数学论文中有不少错误的结论。最早的四色定理“证明”于1879 年做出，10年之后被发现是个错误证明。20 世纪初的一篇论文收集了整整130 页由主要数学家在1900 年以前所犯下的错误。现代数学研究中有些定理的证明非常冗长复杂，难以检验其可靠性。比如，数学家阿尔姆格伦(Almgren) 写了一篇长达1728 页的重要论文，从写作到发表花费了30 年时间。数学家对检验该

论文中复杂证明的正确性缺乏信心。

形式化数学的主要作用是用计算机检查数学证明中的错误，确保数学证明本身的正确性，帮助数学家及时纠正证明中的失误，让他们有更多的精力去发现新的数学定理。

支持形式化数学工作的软件工具称为证明检查器。在证明检查器的支持下，数学家可以把数学公理、定义、引理和推理规则等知识用严格的逻辑语言描述并存入数学知识库中。证明检查器对输入对象进行语法检查，并对数学证明的正确性进行自动验证。在证明开发的过程中，逐步建立一个可重用的数学定理库，汇集所有已经证明的定理，并且支持对新定理的证明。形式化数学需要把所有数学领域的数学知识建库，这个过程有着巨大的工作量。

虽然形式化数学是一项艰巨的工作，但几十年的发展历程显示了它的可行性。表1 是通过了计算机证明检查的一批有代表性的

数学定理。N ＝ p×q  exp(O(logN)

1.     数图和奖励、子站菜单现在必须在鼠标移动到字上才有链接，改成在一块区域内就可以点击。