首页 >> 数学 >> 文章


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

——《Littlewood文集》


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

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

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

到了现代,这个问题更是严重得多,数学的复杂程度和专业化程度已经使得任何一个分支的专业人员数量同证明的普遍难度完全不成正比。这种矛盾在某些极端的例子里尖锐到了荒谬的程度:图论中的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.,任何一个数学家都明白这三个字母的含义:这是拉丁文的缩写,意为“证毕”。

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

证毕。

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


参考资料:

Formal Proof,作者T. Hales
Formal Proof --- Theory and Practice,作者J. Harrison
Formal Proof --- Getting Started,作者F. Wiedijk
(以上三篇为综述文章,见美国数学会通讯2008年11月号)

QED工程网站:http://www.cs.ru.nl/~freek/qed/qed.html

相关软件介绍及下载:
http://coq.inria.fr/
http://mizar.org/
http://www.cl.cam.ac.uk/~jrh13/hol-light/
http://prover.cs.ru.nl/login.php

0
为您推荐

87 Responses to “形式证明:机器的光荣与人的梦想”

  1. “计算机一般被认为是数学家最引以为豪的发明之一,然而当它转过头来开始侵蚀数学家的传统领地时,数学家们的首要反应便是捍卫自己的尊严。”——哈,这种感觉,在哪个学科都是一样的。做科学的一个目的还是显示人的智慧是多么独特和优越,人的思维多么美。

    • 木遥说道:

      数学尤其喜欢这样标榜。。。从雅可比的时代就有一个口号:为了人类心智的荣耀。这句话一直流传到今天。。。

      • 猛犸说道:

        《皇帝新脑》中有句话甚好:

        正是思维的能力,使我们超越了我们体力上的限制,并因此使我们比同伙生物取得更加骄傲的成就。如果机器有朝一日会在我们自以为优越的那种重要品质上超过我们,那时我们是否要向自己的创造物双手奉出那唯一的特权呢?

        • Metaverse说道:

          彭罗斯在那本书里企图说明有些方面,计算机是无法代替人脑的,因为存在某些不能用算法解决的问题,甚至还牵扯到量子力学上来。。。看证明的时候总是很流畅的“因为这个所以有那个”,但为什么“因为有这个”就会想到关联的并且是方向正确的“那一个”,从来都没有人说得清楚。那个“灵光一现”的过程如果能写成算法程序,那数学家就真的可以全部改行了。

        • 看看,还真是每个学科都这么想。

  2. llzzll说道:

    我们都曾经面对过无从下手的证明题目而摇头叹息过,也都在阅读一个自己想不出来的证明过程时体会过那种羚羊挂角无迹可循的美感。

    真的是这样..当看到一道几何难题的时候,想了很久都做不出来,后来看下答案,惊呼一声:绝啊~~

  3. wilddonkey说道:

    好!
    这里涉及到了一个本质的问题:人的智能是否能被计算机彻底实现?
    我又冲动地想把自己的文章贴出来了,看到好文章,又与自己的文章相关就会这样。。。。。。

  4. 小菊说道:

    写的太好了…看的我想哭……

  5. Robot说道:

    还记得当年老师讲到计算机四色定理证明不被接受时的愤愤不平,感觉被数学家们鄙视了。

    • 木遥说道:

      证明四色定理的那些人也是数学家啊。。。

      • 八爪鱼说道:

        原来数学家内部也分个三六九等啊。我还以为只是脑外歧视普外,普外歧视肛肠,肛肠歧视口腔,口腔歧视妇产呢。(妇产无可歧视,只好歧视产妇家属)

        • 木遥说道:

          数学家不分三六九等,只分两等。自己从事的分支是高等,别人的是低等。。。。。

          • 八爪鱼说道:

            希望我不要成为一个女数学家的家属。

        • 木遥说道:

          不过为什么是肛肠歧视口腔。。。。难道不应该是相反么?

        • 李清晨说道:

          脑外才该被歧视呢,虽然死的人最多,但基本死了也白死,大家都觉得开脑壳了,不死算拣着……普外你开肚子把人开死一个看看?
          普外乃现代外科的龙兴之所,谁敢歧视普外?八爪鱼?逮住你的话就把你放烧烤架上烤了吃!另外,肛肠外科是普外的分支……你这个伪内行。
          术业有专供吧,行行出状元。庙小妖风大,水浅王八多,尽力往大庙奔吧~

        • 金色葡萄说道:

          黄金圣斗士飘过

    • 小菊说道:

      。。。robot,你的脑袋分明是在嘲笑我的头像= =b

  6. 卷心菜说道:

    写的非常好,看到最后一句证毕简直让人热血沸腾。

  7. 苗子说道:

    好久没有来松鼠会了,一来就读到一篇这么棒的文章,要顶啊~虽然自己不懂数学,但是对着“为了人类心智的荣耀”的事业还是会莫名激动~

  8. 胡天翼说道:

    写得太好了!既生动又深刻!

  9. water珊说道:

    抿一口咖啡,静静的等待电脑有证明定理能力那天。

    那时候,全世界的数学家就可以好好的休息一下了。

  10. 小津巴说道:

    还是觉得抓紧落实建立人脑和计算机的联系工作,让人脑与计算机这小两口无缝结合,你中有我,我中有你,情意浓浓最靠谱···反正在认知方面那样的二一子脑袋应该相当完美

    • likrrr说道:

      那时中了计算机病毒,口服个抗病毒药物就行了,也不用恢复备份啥的了

      • 小津巴说道:

        那时必然有更广义的“安全套”了吧··淫笑过

      • 真科幻,不错。

      • Metaverse说道:

        换个角度说,那样人也会被动地参与到病毒传播——某个病毒完全可以令人一见到电脑就条件反射地噼里啪啦狂敲键盘吧代码变成EXE变成邮件散布出去。。。

        • Netson说道:

          我觉得真的到那个时候人和人之间的交流说不定也直接连条线就可以了……还用得着这样传播病毒么……

  11. limbo说道:

    数学学障碍者拜倒,再拜!

  12. heavenzhh说道:

    虽然高考时数学仅打了50分,但是仍然喜欢这篇文章。虽说计算机的计算能力已经非常非常强大,但是对于生物脑的模拟程度还是很低。对于“创造”,我觉得电脑仍然是计算了无数种可能的情况下,选择了最优化的结果。

  13. 工人朋友说道:

    现在探讨计算机超越人脑还为时尚早吧!我个人认为在计算机能创作出一流的诗歌之前,我们对大脑的认识依然是很粗浅和未窥套奥的,诗歌所蕴含的不仅仅是智商和知识的积累,还有某种我们称之为情商的东西。我们现在对人脑进化历程的精髓部分的认识还没入门呢!

    • Robot说道:

      艺术创作是一个很难捉摸的东西,通过数据挖掘(data mining)等分析方法,人们发现可以从很多音乐杰作中找到一定的规律来,计算机已经能够成功地创作出很棒(不知道能否算一流)的音乐来。诗歌或许也指日可待了吧。Google "robot composer"可以找到相关内容。

      • 工人朋友说道:

        所以我不说音乐,说诗歌,因为诗歌是语言的高级表现形式,而语言又是一种无穷组合且更新速度特别快的东西,它所涉及的精度和广度都是音乐无法比拟的。

        • likrrr说道:

          诗歌才不难吧?像朦胧派的,只要有无边无际的想象力,就是猴子写的诗歌也是可以欣赏的

          • Justso说道:

            只要计算能力不断提高,未来什么都能算出来。就连说不准的天气也是如此。100年前我们还不知道自己能不能算不出来天气,但未来,这就不好说了。

      • 不知道为什么,我特别抵触这种音乐。。

        • likrrr说道:

          深埋在潜意识里的人的自尊。

        • Justso说道:

          你抵触也没用,这些规律都上了音乐学院的教科书,所谓的音乐家用这样的处方已经开始批量生产音乐了。

    • 木遥说道:

      文章里没有提到计算机超越人脑的问题啊。不要说艺术,即使在自然科学问题上让电脑“做研究”也是遥不可及的事情。这篇文章的全部话题仅限于数学领域而已。

  14. fwjmath说道:

    自动证明程序的存在是不是违反了停机定理?~~~

    • 混沌说道:

      我同意你的说法!
      哥德尔所说,“数学不仅是不完全的,还是不可完全的”,这一点也恰是哥德尔定理最深刻的哲学义蕴。
      著名数学家外尔(H.Weyl)就此感慨:“上帝是存在的,因为数学无疑是一致的;魔鬼也是存在的,因为我们不能证明这种一致性。”

      • fwjmath说道:

        呃……我这个是纯学术性的问题……
        我觉得应该违反停机定理,但是不是太肯定我的构造对不对……

        • 木遥说道:

          其实我也每次看到哥德尔这个词就忍不住要呃一下。。。哈哈~

          • fwjmath说道:

            这人的这定理是数学家的梦魇啊……

          • wealk说道:

            ... 不是数学家的 大多数数学家都 庆幸 这个定理是对的
            说是梦魇的 那是希尔伯特的梦魇

    • 木遥说道:

      人也是机器,人能够自动证明一个数学定理算不算违反停机定理?

      停机定理并没有限制机器真的去证明一个定理阿。反过来,这篇文章中也没有说机器可以证明或者证伪“任何”定理,人也做不到这一点。

      • fwjmath说道:

        对于某一个定理来说当然没所谓~~~我的意思是所有的话恐怕就不行而已~~~
        人是不是图灵机这个事情其实还是需要斟酌的……反正在漫长的一段岁月里我们恐怕是不能知道答案的……

    • wealk说道:

      没有 停机定理 一个程序判定所有的程序是否停机 自动证明 肯定只是 判定一些了

  15. yami说道:

    文字太美了,行云流水啊,尤其喜欢结尾的阅读感觉。

  16. 混沌说道:

    看着的确让人激动!

  17. touch说道:

    Q.E.D一词很让人心潮澎湃啊。

    形式证明难有突破性贡献,人类自身都不能一些显而易见的思考过程逻辑地表达,更枉提更加抽象的类比联想等等那些反逻辑的更“玄妙”的思考过程了,而这些正是创造性的来源。不过形式证明作为定理验证机还是很有前途的。数学家在很长一段时间内还是很安全的,起码一流数学家是。

  18. 小如说道:

    喜欢结尾,幽远又让人心潮澎湃。

    PS:……证毕。
    (想象一下计算机说出这两个字的感觉……)

    想起小时候看的《电脑娃娃》,喝了杯饮料:“我的电路湿了……”

  19. Justso说道:

    “人们对形式证明的批评多半集中于它极端的繁琐和不直观。然而,既然人们已经知道如何把一个传统证明翻译为形式证明,那么把一个计算机生成的形式证明翻译回人们可以直接阅读和理解的直观证明在理论上说来也并非全然不可能。”

    这句话过于乐观了,通读整篇翻译文章,还是觉得有个问题没说明白,那就是形式证明与传统证明之间区别过于科普的叙述,换句话说,这个鸿沟目前还太深,太深。从1940年代,到2000年代,最大的一个区别是计算成本下降了足有几亿倍,人类能够达到的计算能力甚至超过了几亿倍,这导致了近年,很多海量计算的证明可以实现了,比如四色定理的证明。

    尽管楼上那么多人都说这文章不错,我却真的看糊涂了。记录了不少有价值的信息,可以按图索骥,但数学科学界真正的突破,貌似还真是没有。是不是这样呢?

    • fwjmath说道:

      可读证明(就是传统证明啦)在某些问题上是比较可行的,比如说张景中在初等几何中用面积法等一系列手段进行的一类机械证明方法产出的就是可读证明~~~
      别的领域上就不清楚了~~~
      其实我觉得这个“形式证明翻译成可读证明”是非常困难的……

      而且我个人认为,可读证明比起形式证明的优势就是简洁有力。它的起点不一定和原来的问题有什么关系,但是在整个过程中突然峰回路转,风云突变,灯灯灯凳……然后就是结论,整个过程不超过两页纸。
      形式证明那就麻烦了……那真的是电话本……

      • 木遥说道:

        几何机械化是吴文俊先生带领出来的有中国特色的一个流派,说起来当然也是机器证明,但是其思路和本文所说的formal proof还是有区别。吴先生的口号是“把质的困难转化为量的复杂。”,量都复杂了,想不是电话本都难啊。

        但是一般的形式证明则未必如此,或者说,并不能说形式证明就一定无法用可读的形式表达出来。事实上,今天的形式证明大多数就是由人的原始证明直接翻译过去的,它们和直观证明只在叙述方式上有区别,证明的理路其实是一样的。

        • Justso说道:

          哦?这和我的直觉正好相反,我以为传统证明与现在的计算机证明分别代表了质和量两个方面,而计算机代表的形式证明多数(我所知的几个证明,比如四色)用穷举量 + 可读形式进行演算。而且因为其直观和穷举特点,被传统数学家认为不严谨,也不够完美所反对。

          这里的质和量和平时说的质量还不一样,只是区分称谓。

  20. Justso说道:

    我想起来了,十年前我看过类似内容的文章,就是讲传统数学家对穷举等方法为基础的计算机演算来证明的数学定律持否定与怀疑态度。实际上,这个问题至今还在争论,而本文实际上说的就是这件事,对不?还说了什么?如果我没说清楚,请告诉我。

    • Netson说道:

      貌似不是吧……
      当然四色定理的证明是穷举……
      但是文章里面说的最终目标貌似不是用穷举的证明……

      • Justso说道:

        问题就是,文章中说的到底是啥呢??

        • Netson说道:

          我个人认为(或者说,理解)文章说的应该是和数理逻辑类似的东西……将我们已知的条件(公理、定理等)转换为数理逻辑符号去让计算机推演……然后将计算机推演出来的定理再用人类的语言表达出来……

  21. 御主人様说道:

    目前人类的灭绝已成定局
    人类终将慢慢演变(如果自己不先相互种蘑菇的话)成另一种完全不同的生物

    同当初将线粒体吞噬入体内一般
    人类掌握了工具,并将其作为自己手臂的延长
    我不太认同将计算机看作是自己的威胁的看法
    在我看来,计算机本身就是人类的一部分
    当然,这个“人类”是一个相当广义的“人类”

    在经历了漫长的自然进化之后
    人类将要面对应该就是人工选择的进化了
    而计算机进入人体几乎是不可避免的

    当然,未来有很多可能的发展方向
    也正因为无法揣测时代的车轮将滚向何方
    世界才会显得比较有趣一些

  22. xiphoid说道:

    写得好啊。文章本身就像一首诗。

    我想1976年对四色定理的机器证明应该不是机器证明的典型吧。机器证明是神圣的事业,而验证几千个图的性质听起来让人厌烦。

    如果上帝真的存在,一定会为人类发展机器证明而震怒,因为这是 “老头子” 最大的秘密。

    • 木遥说道:

      我文中说了,1976年那个证明不算是严格意义上的机器证明,只能算是有机器参与了的证明。见“2005年,Gonthier建立了四色定理的全部电脑化证明”那段话。

  23. likrrr说道:

    对数学家们的葱白之情犹如长江之水,滔滔不绝...

  24. skyswind说道:

    穆遥遥!照片越选越有水平了!

  25. hqwxyz说道:

    数学在某些方面是可以通过验证方式证明的。《数学与哲学》中举了一个例子:(x+1)*(x-1)=x^2-1。通过代入1、2、3后看到左边=右边,那么通过代数基本地理可以知道那是一个恒等式。

    • likrrr说道:

      这个这个..
      根据我这个数学永远处于高中水平的人看,不太可靠,怎么判断迭代几次就算通过验证了呢?

      • cc21说道:

        验证3次就够了。
        原来的等式是一个最高次不超过2次的多项式求根,复数域上最多2个根,所以如果有3个不同的数值满足等式,那就说明原来的多项式就是零多项式。
        只是,代数基本定理可是太深刻的定理了。和这个要证明的例子相比不是一个等级的,有点高射炮打蚊子的感觉。

  26. 二流仙说道:


    用康托尔的话说
    “我看见了它,可我不相信它”
    不过
    为了人类心智的荣耀
    无限憧憬ing
    智慧为认知划定了界限
    有些事我永远不想知道
    俺们或许该跟老头子叫板哒
    一颗符合进化论的大脑已经不够用哒

  27. opq说道:

    荣耀属于变速箱

    已知事实:当地时间午后2时13分,在热闹的大街上,一个身份独一无二的半大小子跑进一条小胡同。
    求证:此人绝非打算上厕所。

    用已经得到的全部相关条件来组织逻辑关系,毫无偏差地让综合反应结果指向特定事实并不困难。
    为还不知道是否遗漏的零散齿轮寻找不可或缺的当事伙伴,组合成加工出明确结果的机器,而且杜绝错拿本来不参与的同功能零件的错误,是最艰难的逻辑导航任务,与门非门好开,在或门的歧路上不知道跑掉了多少只羊,又误抓了多少只狗。脑袋在独木桥上最会行走,也可以坐火车沿着唯一轨道前进节省精力,但是要躲在卧铺睡大觉,让火车自己正确选择岔路,就近似迷宫问题了;如果和罗马城之间没有现成的铁轨,就变成新逻辑环节铺设问题了,可行和实际所行又是麻烦。
    倒过来穷举,认定公理体系已经绝对正确和完备,一切齿轮都参加装配,排列组合制造所有自洽的坦克,让它们各尽所能越野行动,找出连接起点和终点的轨迹,也能找到合理的路线,只是那么多齿轮和外加条件让可行路线极多,岂止五个参数让大象摇鼻子那么简单,于是显露出密码破译问题的狰狞斑纹....难怪有个雕塑托着腮帮直皱眉,因为屁股下面坐着一个看不见的黑箱。

    宇宙是个宇宙,脑海是个宇宙,逻辑世界也是一个宇宙

    雷毕

  28. afong说道:

    写的太好了!当年老师提到吴文俊的机器证明,原来是这么回事啊~~

  29. 金色葡萄说道:

    准备被证明的定理,可以随机产生么?然后交给机器去验证

    定律的数量是有限的么?

  30. 冲孔板网说道:

    图片做的太诱人了 就算不是真人 也一样被迷惑

  31. sumerian说道:

    看得心潮澎湃啊!
    但QED项目好像已经宣告失败了……

Leave a Reply