我们能用计算机程序来检查数学定理的证明吗？

 

“在我看来，在传统的人类审查与计算机验证之间的选择，就像科学上在日晷与原子钟之间的选择一样。”——汤姆·海耶斯(Tom Hales, 参见 [4])

 

“由于计算机与人是非常不同的，计算机的快速进展促使这点发生了戏剧性的变化。例如，阿佩尔(Appel) 与哈肯(Haken)使用了巨量的自动运算完成了四色定理的证明，引起了大量的争论。在我看来，这些争论几乎不涉及到人们对定理的真实性或者证明的正确性。这反映出了，除了对‘定理是正确的’这种知识以外，人类还想要理解定理，这是一种持续的欲望。” ——比尔·瑟斯顿( Bill Thurston,参见[6])

 

 

一个机器检验的证明(machine-checked proof)是在叫做“证明助手”(proof assistant)的软件中撰写的证明。这个证明助手保证了撰写的明证之于“数学公理”与“逻辑规则”是可以编译的。在定理证明中使用计算机的影响是两极化的。关于这个话题，上面的引用代表了涉及到这个主题的一些观点。

 

1.到底什么是计算机辅助证明？

 

2.使用计算机来证明定理有什么长处与缺点？

 

3.对证明助手的学习使用有兴趣的人，应该如何起步呢？

 

 

动机的问题

 

计算机辅助的证明是一门技术。当时使用旧技术不能解决一些问题的时候，数学家就会关心新技术。这就是我们的动机的问题：

 

 

 

我们来看两个已经解决了的问题。第一个是魔方。第二个是安德鲁·怀尔斯(Andrew Wiles)作出的费马大定理的证明。

 

证明丢番图方程与解魔方之间有一个很大的差别：当一个人解决了魔方的问题，他立即知道问题解决了，然而怀尔斯的证明花费了几个月的时间来进行正式的审查。

 

 

随着我们数学教育阶段的提升。我们检查答案的能力在下降。比如，我的启蒙数学课是我母亲教我的数数。就比较小的加法来说，我可以使用数手指的办法来检查我的答案。从一到十的基本数字以及用手指验证答案都是母亲教会我的。一个人学会了解代数方程，也就学会了使用变量代换来检查答案。检查微积分就更加的棘手了，我们尚可以对Wolfram Alpha报以比较大的信心（译者注，Wolfram Alpha是一个数学软件，可以做符号运算。具有计算积分的功能，还能告诉你得到答案的步骤）。至于实分析与抽象代数，学生们最终是把作业交给老师，看看教授们是否相信他们的论证，这样来检查他们的作业正确与否的。

 

 

什么是证明助手?

 

一个计算机证明助手可以对数学论证做更加系统化的检查。用户使用半形式化的语言(既不像形式逻辑那么形式化，也不像日常数学那么非形式化)来撰写他们的证明。证明助手基于某些数学基础来检查证明。正常情况下，我们想起数学基础，我们想到的是集合论。然后由于技术的原因，证明助手是就“类型论”的基础来实现的。在提出ZFC集合论的大致同时，罗素与怀特海提出了类型论作为另一个数学基础。有不同的数学基础，这在哲学上产生了不同的影响。对于我们来说，这是有争议的，我们在这个问题上就此打住。

 

 

下图展示了证明助手Lean中的一个正确的证明与一个不正确的证明：

 

 

红色错误信息已经很清楚地显示了上面的证明是错误的。下面的证明，由于没有错误，可以迅速看出是正确的。就像魔方一样，一个证明是否正确可以很清楚的看出来。

 

 

这看起来有点复杂。这是必须的吗？可能是。比如，海耶斯的开普勒定理的证明由于太复杂而不能让期刊编辑来检查。那个证明最终是用证明助手HOL-light来检查的。那个形式化地验证开普勒猜想的计划叫做Flyspeck计划。Flyspeck花费了几年数年时间与微软Azure Cloud 五千个处理器小时才完成。一些人期望一个不那么重度依赖于计算机的证明，以便数学家可以阅读那个证明。

 

乔治·贡蒂尔(Georges Gonthier)及其微软研究院的同事作出了第一个经过形式验证的四色定理的证明。这个不同于那个最开始的基于计算机的四色定理的证明。本质上，那个原始的证明是拥有非常大量的计算机计算的标准数学论证。贡蒂尔的工作审查了这一点：支撑四色定理证明的算法，事实上，做了我们相信它做的。

 

 

费特-汤普森奇阶定理(Feit-Thompson odd order theorem)，是有限单群分类的基石。贡蒂尔的团队使用证明助手Coq形式证明了它。费特-汤普森奇阶定理的原始论文有255页。这个团队其它被高关注度的项目还包括素数定理、哥德尔不完全定理以及中心极限定理的形式证明。

 

 

如何起步？

 

 

这些工具并不是只能用于那种耗费数年的大规模的证明。也存在一些库包含了如下学科的定理与定义：实分析、一般拓扑学、表示论与抽象代数。在工业界，证明助手也用于验证软件与算法。这是非常强大的。一旦一个人可以用数学上严格的方式来宣称“这个程序P没有缺陷(bug)”，他就能证明这件事。利用形式证明软件，程序员可以确信他们的程序是没有错误的。

 

市面上有很多证明助手软件供人使用。它们都是免费的。

 

Isabelle-HOL是劳伦斯·保尔森(Lawrence Paulson)编写的一个证明助手。它基于高阶逻辑。Isabelle 拥有大量可以使用的库以及一些强大的"自动化技术"。这里自动化技术指的是证明助手能为你自动找出一些比较短的证明。HOL-Light是约翰·哈里森(John Harrison)所写、拥有更小的内核的类似程序。

 

Coq 与Lean都基于依赖类型论。开发它们的团队分别被蒂埃里·科康(Thierry Coquand) 与 里奥·德·莫拉(Leo de Moura)所带领。依赖类型论意味着数据类型可以依赖于其它数据类型——这正是我们所希望的。例如，对于任意的k, 我们希望有这么一个类型Fin(k)，它是成员基数为k的有限集合。这些证明助手，即使是近期发布的，自动化能力也较弱；由于技术原因，在依赖类型论中实现自动化，是更困难的办法（至少目前是这样）。

 

上面提到的证明助手都有在线手册。Lean 2有一个交互式的网页版教程(https://leanprover.github.io/tutorial/)。Lean的当前版本号是3，不过笔者发现阅读这个教程是总体上品味证明助手思想的好方式。

 

 

问题与展望

 

对于一线数学家来说，证明助手当前还没有好到可以让他们自如的使用的地步。海耶斯确实在他的开普勒问题的工作中使用了HOL-light，不过，除非数学家迫不得已，他们是不愿意做这样类似的事情的。当前的库，还没有足够大到包括关于日常定理的日常论证。例如，我们本来想证明一个关于紧李群的标准结论，发现哈尔定理(Haar’s theorem，证明哈尔测度存在性的)不在我们的库里。这个定理经常被引用，它的证明冗长，而且，就当前的技术来说，得到我们希望的那种形式证明还需要花费数年时间。

 

还有另一个更加本源的反对理由。用瑟斯顿的语言来说，数学，最终是关于数学对象的理解，防止我们的理解走入迷途的证明仅仅是第二位的。用伟大的组合学家罗塔(G.-C. Rota)的话说，“说一个数学家‘证明了定理’就像是说一个作家‘写了一串单词’一样”。他的意思是，算法化的“证明搜索”那种形式的论证不是我们所想要的。

 

不过，并没有什么证据表明，一个人理解数学对象与使用计算机证明助手是相冲突的。机器检验并不是证明搜索的同义词。当前，期刊有人类审查员来检查细节的技术性的论证。如果能够使用计算机来检查这些，我们损失任何东西，反而得到了更多的可核查性。

 

 

史蒂芬·沃尔弗拉姆(Steven Wolfram)最近对形式证明产生了兴趣。沃尔弗拉姆的团队已经在努力工作以使Mathematica与形式证明合作[1]。相关的语言学家、计算机科学家以及数学家时常在考虑那些让计算机代码看起来更像日常数学的方法。最终目标是提高审查过程的效率。

 

 

所有的期刊都要求我们使用LaTeX来写论文——虽然并不一直如此。也许在未来，一些期刊将会为了计算机检查而要求半形式化语言的证明。那样，期刊编辑将把更多注意力放在清晰性以及数学文章的总体展示上面——这就是加深了人类对数学的理解。

 

 

 

致谢

 

我对卡耐基梅隆大学的杰里米·阿维加德(Jeremy Avigad)和匹斯堡大学的汤姆·海耶斯(Tom Hales)致以最大的感激，是他们教会我我所知道的关于证明助手的知识。 我同样对约翰霍普金斯大学的艾米利·里尔(Emily Riehl)表示感谢，是他让我知道了比尔·瑟斯顿(Bill Thurston)的《论证明与数学的进展》(On Proof and Progress in Mathematics)。这篇杰出的文章，我在本文中引用了多次。最后，我把这个笔记献给晚年的弗拉基米尔·沃沃斯基(Vladimir Voevodsky)。我个人从未见过他，不过，他给我的多位老师的影响，他的论文，他的讲稿记录，都是我的本科教育中最重要的东西。

 

 

 

 

 

原参考文献

[1] Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. Intelligent Computer Mathematics, 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings.

[2] Gonthier, G.: Formal proof—the Four Color Theorem. Notices of the AMS 55(11), 1382–1393 (2008)

[3] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Fran¸cois Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry, A machine-checked proof of the odd order theorem, Interactive Theorem Proving – 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings (Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, eds.), Lecture Notes in Computer Science, vol. 7998, Springer, 2013, pp. 163–179.

[4] Hales, T., & Hales, T. C. (2012). Dense sphere packings: a blueprint for formal proofs (Vol. 400). Cambridge University Press.

[5] Hales, T.C. Introduction to the Flyspeck project. In Thierry Coquand, Henri Lombardi, and Marie-Franc¸oise Roy, editors, Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2006. Internationales Begegnungs- und Forschungszentrum f¨ur Informatik (IBFI), Schloss Dagstuhl, Germany. http://drops.dagstuhl.de/opus/volltexte/2006/432.

[6] Thurston, W.: 1994, ‘On Proof and Progress in Mathematics’, Bulletin of the American Mathematical Society 30(2), 161–177.