定理机械化证明

姓名：李嘉蔚 学号16020520034

【嵌牛导读】：电脑打败围棋高手，电脑会深度学习。人类的智慧与尊严遭遇挑战。

【嵌牛鼻子】：吴文俊，哥德尔不完备定理，人脑。

【嵌牛提问】：电脑能与人类一样研究数学吗？有什么用呢？

【嵌牛正文】：

定理机械化证明

2011年，一场“数学之争”让很多人至今仍记忆犹新。

华中科技大学的一名新生致信校长论证文科是否需要学数学。

正可谓一信激起千层浪，一时间，关于学习数学究竟有何意义的讨论在学术界广泛展开。

数学的意义何在？是否真的犹如“屠龙之技”一般毫无用武之地？

“应用是数学的生命线，这是我一直保持的观点。” 中国著名数学家、中国科学院院士吴文俊如此回答。

“数学里，有人类最基本的智慧。”吴文俊的得意门生、中科院数学与系统科学研究院研究员高小山这样说道。

在吴文俊长达几十年的数学研究之路上，在拓扑学、机器证明、代数几何、中国数学史、对策论等研究领域均有杰出的贡献，在国内外享有盛誉。

原本，就连吴文俊都以为自己会在纯数学的研究道路上一直走下去，却没想到这条路在上世纪70年代出现了转折。

1971年，吴文俊被下放到北京海淀区学院路附近的北京无线电一厂劳动，也就是从这个时候开始，他对数学有了与以往不一样的感受和理解。

当时，北京无线电一厂正在生产电子计算机，这让第一次接触到这一事物的吴文俊在倍感神奇的同时也多了很多思考。

“在工厂里，我看到了计算机的威力。”吴文俊说，“把数学方程输入进去，结果立刻就能算出来。我被这样的威力震惊了，就下决心学计算机，同时也觉得，把计算机用好，可以解决很多问题。”

于是，在近耳顺之年，吴文俊毅然开始学习计算机。

1977年，吴文俊引入了一种强大的机械方法，将初等几何定理证明问题这一自动推理经典困难问题转化为多项式的符号计算问题，由此得到了有效的机器证明方法。

在吴文俊之前，几何自动推理占统治地位的方法是AI搜索法，此方法被证明在计算效率上是行不通的。通过引入深邃的数学想法，吴文俊开辟了一种全新的方法，该方法被证明在解决一大类问题上都是极为有效的，而不仅仅局限在初等几何领域。

那么，究竟何为数学机械化？

所谓“数学机械化”，就是把数学中的方程求解与定理证明转变为计算机可以接受的形式，并利用计算机强大的计算功能解决数学与高新技术中的理论问题。

换句话说，就是用计算机做数学研究并让计算机更智能化。

随着计算机技术的飞速发展，人类脑力劳动的机械化有了实现的可能性，部分实现脑力劳动的机械化，可为科学研究与高新技术研究提供有力工具，使科研工作者摆脱繁琐的甚至是人力难以胜任的工作，进行更高层次的创新性研究，从而提高知识创新的效率。

由此诞生的数学机械化研究，不仅为数学的发展提出了一种新构想，也将为信息技术的创新发挥重要作用。

不久，这一方法再次被普遍应用于智能CAD、机器人、计算机视觉中。

定理机械化证明

计算机科学被认为是算法的科学，而算法研究的本质是数学问题。计算机在很多领域的应用，如图像传输与压缩、复杂的曲面造型与加工、信息安全中的编码与密码等都在呼唤新的数学方法。

这些挑战为数学快速发展提供了前所未有的机遇，而数学的研究将为解决许多高科技问题提供有力工具。

如今，通过研究，高小山带领学生已经将特征列、稀疏结式与周形式等数学机械化的核心方法开拓到微分与差分情形；在几何自动作图与微分消元法方面开发出了在国际上领先的软件；针对数控系统核心功能，开发了时间最优的插补算法，显著提升了数控加工的效率与质量等。

很遗憾，吴文俊先生已经去世。

不禁要问人工智能会代替数学家吗？

大家可能都被Google的AlphaGo击败三届欧洲围棋冠军的新闻刷屏了吧。既然人工智能在回合制游戏中有相当大的突破，那么在遥远的未来，AI最终能否先于人类数学家给出例如黎曼猜想之类问题的证明？能否构建出自洽且有预言力的终极物理理论或促进数学发展的理论（比如弦论）？

有人觉得是会的：但是那时候人工智能应该可以代替所有人。 而且感觉时间不会太久。

然而我觉得应该不会。因为哥德尔不完备定理。

哥德尔不完备定理”的主要内容可以如下表示：

在任何一个相容的形式化数学理论中，只要它可以在其中定义自然数的概念，就可以在其中找出一个命题，在该系统中既不能证明它为真，也不能证明它为假。

换句话说：一个包含自然数的体系下，存在着一个问题，在该体系的基础公理下永远也不能证明该问题是对的，同时也永远无法证明该问题是错的。

在数学的历史上，曾经多次出现这样的问题。

举世闻名的费马大定理就曾经让数学家陷入这样的困惑。在三百多年的漫长探索中，很多数学家对费马大定理是否能证明或给出反例都表示出了极大的悲观。而另外两个世界知名的数学难题——哥德巴赫猜想和黎曼猜想，由于哥德尔提出了幽灵般的不完备定理，迄今为止，也被少数数学家悲观地预测为不能证明也不能否证的问题。

但是，这也并不表示此类问题就没有解决的希望，只不过是基于数论的基础公理无法证明该类问题而已，人们需要利用其它形式系统的方法来实现跨界证明。费马大定理最后就是利用椭圆曲线的工具才得以完美解决，1995年，英国数学家怀尔斯在潜心面壁8年后终于解决了这个困扰人类358年的难题。

如果哥德尔不完备定理只是在数学领域显示出顽强生命力的话，那么它的影响力要有限得多，而让它真正大放异彩的，是其随后在计算机和人工智能浪潮中的应用 。

数学的基础是建立在一系列的公理之上，在逻辑推理的辅助下往各个方向无限延伸。构成数学推理的语言是一套符号运算系统，在基本公理的奠基下，人们可以依靠逻辑递归地推导出一系列毋庸置疑的结论。

哥德尔不完备定理其实揭示了这种基于数论有限公理的形式主义逻辑的不完备性。即人们可以在其中添加无限多的公理而与之前的公理没有任何矛盾，且这些新加入的公理无法用之前的公理递归枚举得出。这对当代的计算机科学有着深远的影响。

众所周知，现代的计算机都是基于冯·诺依曼提出的二进制数字运算的基本原理和一系列基础公理，其执行一般由输入、处理和输出组成。尽管计算机在速度和执行效率上有了日新月异的发展，但是其处理数据的思路仍然是基于一定的递归规则运算来判断命题的真伪，从而输出结果。

然而哥德尔不完备定理却无情地揭示了计算机的隐患：至少存在一个命题，递归程序无法判断其真伪。系统在处理这样的问题时必然陷入无限卡壳的状态。

解决这一致命缺陷的办法只有无限扩展公理集，但由于计算机的存储始终是有限的，因此我们永远也无法造出完美的计算机。这样，基于冯·诺依曼理论构建的计算机从诞生开始就有着先天的“基因”缺陷。

也正因为如此，一些数学家认为人类的“直觉”不受该定理的限制，所以计算机永远不可能具有人脑的能力。人工智能无论如何发展，也无法具备人类的智慧。

但另外一些研究指出人类思维也是不完备的，人脑的“思考”和电脑的“运算”基本原理一致。

电脑用电子元件的“开、闭”和电信号的传递，人脑则相应表现为神经原的“冲动、抑制”和化学信号的传递。

这种相似的联系直接导致人脑的思考也是符合哥德尔不完备定理的条件的，因此人类的思维系统也是不完备的。

在生活实践中，人们是通过思考来建立对世界的客观认识和描述的，而语言则是人们彼此交流思考结果的有力工具。

对人脑而言，思维推理系统的不完备也就意味着存在不能用思维证实的问题。

简而言之，现实中总有那么一些问题或者想法，我们无法用思维来证实或者否定它，从而也就无法用语言来完全准确的表达我们的思想。由于思维是客观实在的近似反映，语言则是思维的近似表达。

这就是我们“只可意会、不可言传”背后的数学原因。

其实还有一个定理是讲不存在证明一切数学问题的通用方法。

所以我认为人类会去探求新方法，而电脑不会。电脑的机器学习之类的只是受到人脑神经网络的启发，并不是在模拟人脑的运作！

其实人脑应该不是形式系统。

所以计算机除非能完全按照人脑的方式运作，否则是不会替代数学家进行数学研究的。

定理机械化证明

对人类来说，一个在某个形式系统内不可判定的命题，人类可以扩大该形式系统而电脑无能为力。

其实数学不是形式系统，人脑也不是，而电脑是。

因为人类能够理解。比如类(比如所有集合的集合)这个概念，是其实不存在的，而集合是存在的，但是人类既能研究存在的集合，也能理解研究不存在的类。

我国数学家田刚也有与我相同的观点：

定理机械化证明

在作为数学家的田刚委员看来，类似“阿尔法狗”的人工智能产品比人类是有优势的。“数学上或者说从科学上来讲，现代人工智能通过一些数学知识、计算机知识，进行一些优选，它们的机械能力比人类强，”田刚委员分析道，“比如‘阿尔法狗’下围棋时，人们能够想到五六步，但是机器它能算到十几甚至二十几步。”

人工智能机器的产生，可以让我们的生活更方便，也能够减轻人们的工作量，一些很机械、需要知识水平不是很高的工作，以后会被人工智能逐步代替，“比如驾驶，现在飞机很多都是智能驾驶的；再比如原来比较复杂、有危险的工作，都可以被人工智能代替。”田委员说。

从长远来看，人类能够被人工智能所代替的工作会越来越多，比如从理论上可以归纳成某种结构图的工作，机器做起来要比人类快速、精准得多。再比如现在各个国家都很重视“脑科学”，随着对人脑结构的深入理解，一些仿生的机器会更多，因此，人工智能是一个很重要的发展方向。

虽然如此发展下去，人工智能会对人类的就业产生一定的影响，但是在田刚委员看来，人工智能依然并不能完全代替人类，“一些需要人发挥灵感、或者结构更复杂的东西，目前肯定不能完全替代，所以不必太担心。”

但是我们确实希望有一个能为我们代劳的电脑来研究数学，不是吗？