No.419. 你可知道一个出生在中国的华人，孕育了理论计算机科学？

在我有限的认知里，在计算机发展的早期，出生在中国大陆的华人对这方面的贡献是比较少的，毕竟那个年代，中国在社会学方面进行探索，当时没有精力搞计算机。我是说以前，现在当然很厉害了，在量子计算机领域、生命科学领域、中药与计算机结合的领域，已经遥遥领先了，这个不必我多说。我是说以前，上个世纪。但是，有一位出生于中国大陆的华人，是真的开创了人工智能一个相当重要的领域：自动定理证明。

我先来介绍一下什么叫自动定理证明，自动定理证明是一种利用计算机程序来自动化地推导或证明数学定理的过程。这种方法的目标是通过计算机算法和推理系统，减轻人工证明的工作量，提高证明的效率和精确度。

在自动定理证明中，通常使用形式化的逻辑系统和规则，以及数学表达式的形式化表示。常见的逻辑系统包括一阶逻辑、高阶逻辑、模态逻辑等。自动定理证明系统还可以采用不同的推理方法，如归结法、正则推理、模型检测等。

之所以能发展出这个流派，源于罗素和希尔伯特的思想。罗素大家可能比如熟悉，是一位英国哲学家、数学家、逻辑学家、历史学家、社会评论家和政治活动家。他是20世纪初期最重要的思想家之一，罗素的贡献横跨多个领域，他的思想和著作在数学、哲学、逻辑学等领域产生了深远的影响。

我发现，相比于了解罗素的数学和科学，很多人更关注罗素的八卦，我做电台的经验发现的。我就讲点八卦吧。与他的感情生活有关的。这个八卦跟人工智能能扯上联系。

罗素很早就出名了，在1902，作为一个自行车爱好者，他就去骑车了。在骑车的时候，他就思考这样一个问题，他还爱不爱他老婆。罗素的老婆比他大5岁，当时已经结婚7年，七年之痒。他老婆叫Alys Pearsall Smith，于是他回家直接跟老婆坦白了，说我已经不爱你了，离婚吧！

他老婆是个爆脾气，说你要是离婚，我就杀了你，再自杀。直接拿刀要砍罗素，罗素马上就说不离了，（后话是，两人的婚姻又拖了20年，最后还是离婚了。）

罗素要找点事情做，在那段想离婚却怕被老婆一刀两段的日子里，他要写一本书叫《数学原理》，那种痛苦让他在1903年到1904年那两年，天天去牛津的一座桥上看火车，思考要不要跳下去跟火车来个亲密接触。这件事情一直折磨着罗素，夫妻关系，还有跟合作者怀特海之间也有矛盾……总之，一直到1906年，那时候离爱因斯坦发表他那5篇影响人类的论文过去一年了，罗素还在跟《数学原理》较劲。直到写到1910年，手稿写了两箱子，运到了剑桥大学出版社。

人家出版社也是要赚钱的，你这《数学原理》谁买啊。他们做了一个估算，这书要是出版了，要赔600英镑，出版社说你先交600英镑再说吧。那时候100英镑相当于今天的2万美元，也就是说，罗素跟怀特海写了10年书，赔了12万美元，每年赔1.2万美元。后来，出版社肯定是没赔钱的，这部书被评为上世纪非虚构类图书的第23名，虽然没人看，但是销量肯定可以的，每个大学卖一套，中国怎么也得卖了3000套吧，还有世界其它国家呢？

后来罗素自己说，他这三卷书，看完的总共有6人。但是他没具体说有哪6人，只说人为波兰人， 三人为得克萨斯人，然后请大家对号入座。显然，他应该是低估了他的影响力，肯定不止6人看完过，我先声明，我没看完过。其实，为了证明数字1，这本书就花了好几百页面，正常人是看不懂的，如果有兴趣的人可以挑战一下。每所高校的图书馆里肯定都有这部书，这部书共分为三卷。名字叫《数字原理》它通常缩写为PM (Principia Mathematica)。这部书里有一个重要的思想：所有数学真理在一组数理逻辑内的公理和推理规则下，原则上都是可以证明的。

就是这句话，所有的数学真理，原则上都是可以证明的。于是，有人就想用计算机来证明所有的数学真理。早期想这么干的人就是前几期我讲的那对师徒：纽厄尔与司马贺。这两个人参加过人工智能第一次会议，最早期就是研究机器定理证明的。两人还写信给罗素，希望得到罗素的鼓励，罗素也真的鼓励了，说你们加油干吧！

如果了解数学的话，应该了解希尔伯特，我就不再多做介绍了。上个世界伟大的数学家，他的理论跟罗素有点类似，就是机器可以干定理证明的活。当时很多的科学家不是独行侠，而是有伙伴，这个希尔伯特的伙伴就比较厉害了，一个叫格哈德·根岑的家伙。这个家伙是德国人，最崇拜的人是元首，参加了德国导弹的研究，是纳粹冲锋队的成员。最后在布拉格被逮捕，饿死在布拉格附近的战俘营中。在前面416期的时候，我不是讲过爱因斯坦的助手么，同样是助手，有人功成名就，有人饿死他乡。这个与社会阅历跟眼界有关，如果仅从学历跟智商上来说，他肯定是顶级的。

数理逻辑目前主要有四个分支，模型论、证明论、递归论跟集合论，这家伙继承了希尔伯特的理论，自己也成了举足轻重的人物，中国有句古话叫：鸟随鸾凤飞能远，人伴贤良品自高。他开创了数理逻辑的四大分支之一递归论，虽然识人不淑，跟随希特勒，饿死他乡了，但是一码归一码。

罗素写了书出来，用他的话来说就是一本书就是一个罪孽，一本大书就是一个难以饶赎的罪孽。他这本书出来，就有了靶子，他认为正确的观点，自然会有科学家认为不正确，而且这不是咱们网上公说公有理，婆说婆有理的家长理短，而是人家用论文证明你的说法有漏洞。

其中，有个名叫哥德尔。这个家伙跟格哈德·根岑在学术上不好较量，毕竟格哈德·根岑英年饿死了，但是哥德尔在眼光上，那是相当的毒辣，他在年轻时就敏锐在感觉到希特勒这人不行，果断放弃在德国拥有的一切，投奔美国继续做研究。他肯定是看完了罗素写的那本《数学原理》，他觉得罗素这个人治学不严谨，他花了1年多的时间，写下了奠定他日后数学江湖地位的论文《论《数学原理》及相关体系中的形式上不可判定命题》，也就是咱们目前常听到的哥德尔不完备性定理。

我试图讲解一下这个定理是什么意思吧，在罗素的数学世界里，认为不存在无法证明的真命题，只是有些命题很难，没找到方法来证明。罗素感叹的是在数学里，有很多困难目前只能用“不漂亮的理论”来解决。而哥德尔则告诉他，这不是漂亮不漂亮的问题，而是无法证明的问题。哥德尔用《数学原理》的理论证明了数学原理本身就是不自洽的。这让罗素备受打击。

罗素对些只回复了一句话：我一直希望在数学中找寻的壮丽的确定性失落在了令人困惑的迷宫里。从此以后，在罗素的世界里，哥德尔就像消失了一样，在不得不提到哥德尔的时候，他仅仅用了一个词语来表达自己的看法：德国的偏见。是的，因为哥德尔是伤他最深的人，他讨厌德国，所谓恨乌及乌吧。哥德尔靠证明罗素错误而获得大名之后，被接纳进了一个海外流亡德国科学家群体，其中包括爱因斯坦，泡利等人，几个德国人整天开研讨会，罗素一次也没出席，并称之为“德国的偏见”那种研讨会，有什么好参加的。

听众可能会奇怪，不是这期的标题是华人么，不要急，铺垫了这么多，华人就要出场了。这个华人名叫王浩，1921年出生在中国，在他上大学的时候，日本侵华，不得已只能去西南联大数学系读书，跟他一个宿舍的人有杨振宁。他是老师是金岳霖，金岳霖就是爱上梁思成老婆，梁启超的儿媳妇林徽因，但是人家已经心有所属了，他就一辈子跟林徽因做邻居，而没有结婚。我现在跟我初恋女友也是邻居，她去哪，我就去哪，都是跟金岳霖学的。金老师跟李敖是同门师弟，两个人的老师就是被称之为中国逻辑之父的殷海光。如果你觉得你讲话没逻辑，我非常推荐大家去读一下殷海光写的《逻辑新引》，但是不要看简体中文版的，你看了简体中文版的，只会更没有逻辑了。你看看人家小师弟李敖，一生女人无数，再看看师兄金岳霖，一生只爱一个人，那真是两个极端啊。

这个王浩跟哥德尔是朋友，那种最亲密的朋友，我有一本王浩给哥德尔写的传记，名字就叫《哥德尔》。当然了，你只靠朋友，肯定是当不了最伟大的科学家的。可以靠自己的文章，或者靠自己的代码，或者靠学生，王浩这三点全做到了。

在1958年的时候，在哈佛大学，王浩在一台IBM 704机器上实现了一个可以证明数学定理的程序，花了9分钟时间，就证明了《数学原理》中150道中的120道，隔年，改进版本直接把罗素写的《数学原理》上的150道题全给证明了，而且还会抢答了，并且可以进行一些推理，给出自己的定理。王浩后来当教授，培养几个图灵奖，他的学生又继续当教授，再培养图灵奖，于是，他的地位就出来了，然后开始拿人工智能领域的奖。

这一期只是铺垫了一下王浩这个科学家，一般来说，当人们提起理论计算科学的时候，就会想起几个人，而这几个人，又是他的徒弟或者他的徒孙。而他，也确实是第一位把罗素写的《数学原理》那本书上的定理全用计算机给证明的人，我想他肯定看过全部的《数学原理》。

除了他之外，中国人又出了像吴文俊这样的科学家，他一直是数学家，但是在全国上下都搞社会探索的时候，他只能去无线电厂焊接收音机，后来不搞艰难的社会探索了，他才有机会又搞数学。最后在60多岁的时候开始学Basic编程，他那台电脑价值2.5万美元，是杨振宁送给他的。下一期，我想继续讲一下中国人在计算机，主要是在自动计算理论上对世界的贡献。实际上，真是没办法，任你有多聪明，天天让你喊口号扫大街，不可能潜心研究的。这一点，我非常佩服这些科学家，白天去工厂干活，又没有电脑给你用，你只能通过自己想来研究理论，研究出来以后，还要说我这个理论是从中国数学史上找到灵感的，否则不给发表。

这一期到这里，下一期再见。