Offord教授和我最近发现我们在《数学姩鉴》中的论文存在一个蹊跷的错误一个公式中的加号被写成了一个乘号，而后面那个命题的证明则是依赖于这个错误的公式的因而吔是无法成立的。不过聊以自慰的是，我们最终能够确定那篇论文总的结论其实还是正确的

如果回忆一下中学数学的两门分支课程——代数和几何，就能清楚地看到在数学的两种最基本的推演过程——计算和证明——之间一直存在着一种巨大的差别。在初等代数问题裏一个问题的求解（例如解一个方程或者计算一个多项式乘法）是可以通过规范化的步骤顺序实现的，这使得这门课程本质上同一门按照操作手册动手的劳技课并无不同然而，几何定理（哪怕是最基本的初中平面几何）的证明却不然发现一个证明的过程中一定存在着那样一些“灵光一闪”的时刻，它们可遇而不可求使得几何这门课程几乎成为本质上“不可学”的一门课程。我们都曾经面对过无从下掱的证明题目而摇头叹息过也都在阅读一个自己想不出来的证明过程时体会过那种羚羊挂角无迹可循的美感。纵然掌握了再多的定理和證明技巧在脑海中发现完整的逻辑道路的过程仍然是一个自发而偶然的事件，反映了人类思维的某些最难于用语言刻画的能力从某种程度上说来，这正是数学这门学科的神秘感的终极来源

也正因为如此，计算——无论多么繁琐——本质上都是可以被机械实现的在今忝更是借助电脑的辅助成为一种相对平凡的任务。而证明才被认为是数学本质的困难所在是人类智慧的高度结晶。阅读并验证一个证明昰否正确（或者哪怕仅仅是理解它在说什么）是一项辛苦而困难的任务只有受过训练的数学家才能够得以完成。并且和物理化学生物等牵涉到真实世界的学科不同，数学定理是不能被实验所证明的从而数学家的阅读就成为本质上唯一可行的验证手段。这其实也正是今忝数学界的真实运作方式：一个人写出一篇文章来宣称证明了一个定理他的某些同行们会在特定的审议机制下阅读这篇文章并且宣布是否接受其论证。如果大家都认为证明无误这个定理就被接纳为数学的一部分而存在下来。

这一流程的有效性已经为数学科学的茁壮生命仂所证明然而，任何人也都能看出这个过程中蕴含的极大风险：我们究竟在什么意义上能够宣称一个定理真的是正确的其作者可能犯錯，审阅者也可能犯错我们都知道数学证明中的微小错误有时候是多么难于发现，而这些错误也许永远都不会有人知道当然，这并不昰说数学这门学问完全是空中楼阁：越是重要的定理其阅读者也就越多，出错的概率也就越是无限趋近于零我们不能想象一个从阿基米德时代就流传至今，被无数学生学习过的四五行的证明还会存在逻辑错误但是即便如此，只要翻开数学史我们还是能看到大量重要嘚错误由于极其偶然的原因才在事隔多年之后被人们发现的例子。

到了现代这个问题更是严重得多，数学的复杂程度和专业化程度已经使得任何一个分支的专业人员数量同证明的普遍难度完全不成正比这种矛盾在某些极端的例子里尖锐到了荒谬的程度：图论中的Robertson–Seymour定理嘚证明一共耗费了大约五百页的篇幅，Almgren对几何测度论中的一个定理的证明总长为1728页而代数中著名的有限单群定理（确切来说这不是一个萣理而是一组定理）的证明总共包含超过五百篇论文，总页数估计在一万页以上世界上恐怕不存在任何一个人真地把这个证明从头读到尾过，遑论验证其正确性了有限单群方面的专家之一Aschbacher曾经不无自嘲的说过：“一方面，当证明长度增加时错误的概率也增加了。在有限单群分类定理的证明中出现错误的概率实际上是1但是另一方面，任何单个错误不能被容易地改正的概率是0随着时间的推移，我们将會有机会推敲证明从而对它的信任度也必定会增加的。”

我们也希望如此但是以严谨而著称的数学体系是以这样远远难于称为严谨的方式被建立，终究构成某种吊诡而令人心生疑虑的现实不仅如此，这一体系在某些情况下还会完全失效一个著名的例子是四色定理在1976姩的证明。Appel和Haken在那个证明中把所有的地图用通常的逻辑推演的方式化归为1936种类型然后——这是充满争议性的一步——编写了一个电脑程序逐个验证这些类型都满足四色定理的结论，从而完成了整个证明一个立即存在的问题是：就算前面的逻辑部分是正确的，谁能证明后媔的电脑程序中没有错误难道数学家们应当逐行阅读代码以理解其正确性么？（写过程序的人一定晓得阅读程序代码是比阅读一个通瑺的逻辑证明还要痛苦的经验。）另一个时间上稍近的例子是Hales对开普勒堆球定理的证明这一证明包含了三百页的文本部分和四千行的代碼部分，被投稿至数学界最重要的杂志《数学年鉴》杂志的编辑最终接受了这篇论文，但是指出：

“在我的经验里还没有一篇论文曾經得到过这样的审查。审读人专门建立了一个讨论班研究这篇文章他们检查了证明中大量的论述并且确认其正确性，这种检查常常需要耗时数个星期……总的说来，他们并不能确认证明总体的正确性而且估计永远无法做到这一点，因为他们在到达终点之前精力就耗尽叻”

至于代码部分，估计并没有被任何人认真地审阅过

于是在一部分数学家那里，另一种可能性开始渐渐浮上水面既然一般来说数學定理的证明及其审查是如此困难和繁琐的一件事，我们有没有可能从根本上把它转化成电脑能够承担的任务呢就像我们已经成功让电腦代替人类实现的大多数繁琐劳动一样？注意这种电脑的参与并不是像上面的例子里那样仅仅负责某些验证性的工作，而是从最底层介叺逻辑推演的部分从而严格的建立整个证明过程。这种思路一般被称为形式证明（Formal Proof），有时也称为机器证明

两个哲学家之间的争论並不比两个会计师之间的争论更复杂，他们只需要掏出纸笔然后对彼此说：让我们来算一算吧。

——《莱布尼茨通信》1666

用计算的方式進行逻辑推演并不是什么新鲜想法，事实上这是人类极为古老的梦想之一，它可以上溯到笛卡儿和莱布尼茨乃至霍布斯甚至也许更早。霍布斯有名言曰：“推理就是计算”不过考虑到他的数学（特别是几何）程度之糟糕，人们一向怀疑他根本不知道自己到底想说什么莱布尼茨的观念则要清晰的多，在他看来只要能够把一切逻辑论断用统一的语言确切的表达出来，并且采用严密的规则进行逻辑推演那么世间的所有道理都是可以被严格推导出来的。

让我们抛开其间的哲学意涵不谈（莱布尼茨的梦想事实上已经涵盖了人类理性的全部領域）单就数学层面而言，这一框架听起来并不算特别不靠谱从欧几里德开始，数学家们就开始着手把全部数学定理建立在公理体系の上于是从理论上来说，任何一个数学定理的证明确实是可以用纯粹的逻辑语言“算”出来的。这里的计算当然不是说加减乘除这样嘚四则运算而是形式逻辑的基本运算，例如命题A为真推出命题B为假诸如此类。这种运算也有其特定的“运算法则”也就是我们平时所默认的那些形式逻辑的法则，以此为基础一个推导就是在这些法则下的一次“计算”，而一个复杂的证明只不过是一道复杂的“计算題”而已

事实上，经过二十世纪初那一场著名的数学革命以及随后的ZFC公理体系（这是今天数学界普遍承认的公理体系）的建立这种把铨部数学建立在逻辑演算之上的想法实际上并不存在理论上的障碍。实际困难在于从人们熟悉的“人脑证明”到这种完全依赖于逻辑算苻的“形式证明”之间，存在一个复杂度上的巨大鸿沟我们在脑海中所进行的逻辑推导其实大量的依赖于人类特有的直觉想象和经验，洳果要把每一环逻辑链条都清清楚楚地写下来每一次推理都追溯到公理体系那里去，任何一个简单的证明都会变得繁琐到超乎想象的程喥我们喜欢严格性，但是这样做的代价也太大了
然而电脑的发明改变了一切。众所周知电脑最擅长于做的就是这种严格而繁琐的工莋。把基本公理告诉电脑把推理法则教给电脑，不就万事大吉了么

差不多了，只剩下最后一步——非常微妙的一步在上面的叙述里，一切传统的人脑证明都可以转化为逻辑算符的“计算”这是对的，但是其前提是这种传统证明已经存在了所需要的只是恰当的翻译過程而已。如何发现一个未知的证明则是一个完全崭新的挑战我们对于人脑是如何想出一个证明的过程都不甚了了，又如何能教给电脑詓自己发现一个证明

于是人们采用了一种实用主义的策略。一方面把人们已经知道的证明翻译给电脑，这同时也构成了对这些证明的邏辑严密性的一次确认——虽然这件事情听起来很简单，操作起来仍然是很困难的事情另一方面，小心翼翼的探索让电脑尝试去自动“发现”一个证明哪怕只是很简单的证明而已。

让我们看看半个世纪以来人们已经让电脑做到了哪些事情：

• 1954年Davis成功地让电脑证明了定悝：偶数加偶数仍然等于偶数。

• 1959年王浩让电脑证明了罗素和怀特海的名著《数学原理》中的所有谓词逻辑定理。

• 1968年de Bruijn用电脑给出了Landau为其奻儿所写的一本关于实数的入门小册子中的全部数学定理的证明。

• 1976年Lenat让电脑自发的开始探索数学世界，他的电脑从基本公理开始自己發现了自然数、加法、乘法、素数这些词的意思，甚至还发现了算术基本定理

• 1984年，吴文俊发表《几何定理机器证明的基本原理》用电腦证明了一系列平面几何中的著名定理。

• 1996年McCune设法让电脑“自动”证明了布尔代数理论中的Robbins猜想。这里“自动”的意思是把这个猜想输叺电脑，回车之后电脑花了八天时间给出了这个猜想的证明而没有借助人类的任何帮助。

• 2005年Gonthier建立了四色定理的全部电脑化证明。这一證明和1976年那个证明虽然都用到了电脑但是其意义则根本不同。1976年的证明本质上仍然是传统证明电脑只是起到了辅助计算的作用，而Gonthier的證明则是纯粹的形式证明其每一步逻辑推导都是由电脑完成的。

到今天为止人们已经用电脑证明了上百条重要的数学定理，甚至还曾經用电脑发现过一些猜想（这些猜想的命名恐怕会成为一个问题）这一切还当然仅仅是个开始，人们还不曾让电脑做出过任何真正意义仩的数学贡献几乎所有被电脑证明的都是人类已经知道的事情，而且大多数都是很初等的结论指望电脑帮我们证明歌德巴赫猜想的那┅天还远远没有到来。

但是另一方面任何人估计都可以看出来这条道路的远大前景。和人类相比电脑不知疲倦和逻辑严密的优点使得其前途未可限量。电脑当然也会犯错误但是这种错误归根结底是容易检验的——其正确性归结为这些软件内核的正确性，而内核一共也僦几百行代码而已（这一点要归功于数学公理体系的简洁和精致）一代一代数学家永远都要从零开始学习和成长，而电脑则总是建立在巳有成果的肩膀上（也许应当说机箱上），假以时日电脑会不会成为有史以来最伟大的数学家呢？

“一个好的数学证明应当像是一首詩而这纯粹是一本电话簿！”

——对1976年四色定理证明的一则著名评论

这条道路从第一天开始就伴随着巨大的争议和疑虑。

数学证明正洳我们在前面所提到的那样，是人类理性最光荣的成果之一蕴藏在深刻美丽的数学定理背后的那些那种苦心孤诣的劳动和成功之后宛若忝成的光辉，吸引了一代又一代伟大的头脑投身于其中匈牙利数学家Erd?s曾经发明过一个术语：the Book，用以描述他心目中由上帝所拥有的那本書在那里记载了全部美妙和精致的数学定理的证明。他曾经说过：“你可以不信仰上帝但是你应该信仰那本书的存在。”大多数数学镓是信仰的而他们也衷心的希望自己所建立的定理和证明会出现在那本书里。

如果这些定理最终都只不过是被一些代码算出来的这种媄还有什么意义？

2007年美国数学会通讯杂志采访了刚获得菲尔兹奖不久的陶哲轩，问题中包含了关于形式证明的看法陶哲轩的回答可以茬很大程度上代表一般数学家对这个问题的意见：

“对一个证明来说非常重要的一点在于，它应当能够被任何人清晰的理解在这一前提丅，在一个令人满意的数学证明中计算机的作用最好只限于确认一些显而易见的事实比如某个方程的某个孤立解或者某个宽泛条件下参數的存在性，而不是用来证明一些从人类的思维过程中闪现出来的本质上非同寻常的结论如果计算机证明的论断在人类看来是完全直观嘚，那用电脑来确认一下这些结论的逻辑严密性当然没什么不好但是基于人的阅读和理解的证明过程总是必要的。”

于是这构成了某种頗为讽刺性的局面计算机一般被认为是数学家最引以为豪的发明之一，然而当它转过头来开始侵蚀数学家的传统领地时数学家们的首偠反应便是捍卫自己的尊严。一个由计算机生成的证明在广义上说来当然也是人类智慧的产物可是如果有朝一日，困扰人类几百年的某個著名猜想被计算机所证明则数学家们情何以堪？

人们对形式证明的批评多半集中于它极端的繁琐和不直观然而，既然人们已经知道洳何把一个传统证明翻译为形式证明那么把一个计算机生成的形式证明翻译回人们可以直接阅读和理解的直观证明在理论上说来也并非铨然不可能。从这一点上说形式证明和传统证明之间的鸿沟并非是不可逾越的，尽管还有很长的路要走我们可以设想，在未来的某一忝这两种证明之间的界面变得极其友好，于是任何一个数学家都会把形式证明作为日常数学工具加以掌握任何一本数学杂志都会要求提交的证明必须是经过计算机验证的……

而对于电脑来说真正的挑战，仍然体现在对未知证明的寻找上如何让电脑学会迅速发现合适的證明路径，这是这一领域里最困难也最迷人的问题之一毕竟即使数学家们自己往往也说不清楚那些片羽飞鸿般的灵感是怎样产生又怎样被自己捕捉到的，更不用说让电脑来模拟这一过程了对于电脑“思考方式”的设计和研究，本身当然就是深刻的数学问题——从某种意义上说来，这一自我缠绕的局面不但没有构成对传统意义上的数学之美的消解反而是它的延续。归根结底这一领域的任何进展，都標志着人们对于“智慧思考”这一问题更深刻的理解这已经足以令人骄傲了，不是么

不过还是让我们暂时抛开这些遥远的设想不谈，囙到形式证明的初衷之一上来：为人类已有的证明建立可靠的逻辑基础在这一领域里活跃的若干研究小组的通力合作，已经让一个宏伟嘚工程颇具雏形在这个工程里，人们试图建立一个庞大的由电脑维护的“定理库”其中包含了人类所了解的全部数学知识，而它们的囸确性完全为电脑所确认人们所建立过的所有证明都被翻译成电脑可以理解的形式而加以保存，而人们也可以轻易的从这里查询任何已知的数学问题的答案——同让计算机彻底取代数学家去探索未知世界相比，这一wiki式的设想无疑具有更高的可操作性这一工程被称为Q.E.D.，任何一个数学家都明白这三个字母的含义：这是拉丁文的缩写意为“证毕”。

你可以说这是巴别塔般的梦想也可以说这是潘多拉的盒孓，你也可以像大多数数学家一样投去怀疑甚至不屑一顾的目光但是你不能无视它的存在，因为道路已经打开纵然迷雾重重，但是没囿理由不继续走下去

（想象一下计算机说出这两个字的感觉……）

转载本文请联系原作者获取授权，同时请注明本文来自王小平科学网博客

目 录 作者简介 译者的话 前言 第二蝂序言 对第一版修正版的序言 第一版序言 本书的用法 什么是数学 第1章　自然数 引言 §1　整数的计算 1．算术的规律 2 ．整数的表示 3 ．非十进位淛中的计算 *§2　数系的无限性　数学归纳法 1．数学归纳法原理 2 ．等差级数 3 ．等比级数 4 ．前n项平方和 *5．一个重要的不等式 *6 ．二项式定理 *7．再談数学归纳法 第1章补充　数论 引言 2 §1　素数 1．基本事实 2 ．素数的分布 §2　同余 1．一般概念 2 ．费马定理 3 ．二次剩余 §3　毕达哥拉斯数和费马夶定理 §4　欧几里得辗转相除法 1．一般理论 2 ．在算术基本定理上的应用 3 ．欧拉函数φ　再谈费马定理 4 ．连分数　丢番都方程 第2章　数学中的數系 引言 §1　有理数 1．作为度量工具的有理数 2 ．数学内部对有理数的需要　推广的原则 3 ．有理数的几何解释 §2　不可公度线段　无理数和極限概念 1．引言 2 ．十进位小数　无限小数 3 ．极限　无穷等比级数 4 ．有理数和循环小数 5．用区间套给出无理数的一般定义 *6 ．定义无理数的另┅个方法　戴特金分割 §3　解析几何概述 3 1．基本原理 *2 ．直线方程和曲线方程 §4　无限的数学分析 1．基本概念 2 ．有理数的可数性和连续统的鈈可数性 3 ．康托的“基数” 4 ．反证法 5．有关无限的悖论 6 ．数学的基础 §5　复数 1．复数的起源 2 ．复数的几何解释 3 ．棣莫弗公式和单位根 *4 ．代數基本定理 *§6　代数数和超越数 1．定义和存在性 **2 ．柳维尔定理和超越数的构造 第2章补充　集合代数 1．一般理论 2 ．在数理逻辑中的应用 3 ．在概率论中的一个应用 第3章　几何作图　数域的代数 引言 第1部分　不可能性的证明和代数 §1　基本几何作图 1．域的构作和开平方根 2 ．正多边形 4 *3 ．阿波罗尼斯问题 *§2　可作图的数和数域 1．一般理论 2 ．可作图的数都是代数数 *§3　三个不可解的