数学是“科学的皇后”，不仅代表着人类智力的最高挑战，同时也在人类社会和历史发展中起着不可替代的推动作用，可以毫不夸张的说数学已经成为人类现代文明的基石。
数理逻辑是人工智能三大学派之一符号学派的思想源头和理论基础，因此用人工智能方法解决所有数学问题成为了早期人工智能专家关注的重要目标之一。数学的计算机证明与人工智能的发展关系密切，我国著名数学家吴文俊院士从中国数学史的研究中汲取了灵感，是这一领域的早期推动者之一，做出了巨大贡献。
人工智能证明数学定理
1956年，在美国汉诺斯小镇宁静的达特茅斯学院召开了一次用机器来模仿人类学习以及其他方面的智能的会议，这次会议被认为是人工智能的开端，纽厄尔(Allen Newell)和西蒙(Herbert Simon) 在会议上公布了一款被称为“逻辑理论家” 程序(Logic Theorist)，成功证明了罗素和怀特海所著的《数学原理》第二章52 条定理中的38条, 从而开创了人工智能方法证明数学定理的开端。
达特茅斯学院（图片来源：中国人工智能学会https://mp.weixin.qq.com/s/5uJKqu2Xv3LVM2ZFpfsOMg）
仅仅2年之后的1958年，美籍华裔哲学家王浩在一台IBM704计算机上，只用9 分钟就证明了《数学原理》中的一阶逻辑部分的全部350 多条定理, 在当时数学与数理逻辑界引起轰动。当然，纽厄尔和西蒙的“逻辑理论家” 程序使用了“启发式搜索”技术，他们的目标是使用计算机程序模拟出人类智能，而王浩作为数理逻辑学家，他的目标则是通过计算机方法证明数学定理，后来机器定理证明成为早期人工智能发展的一个重要分支。
吴文俊与“吴方法”
在机器定理证明方面，如果说王浩是逻辑系定理证明的先驱，吴文俊院士则开创了几何系定理证明的先河。
吴文俊1919年出生于上海，毕业于交通大学数学系，后获法国斯特拉斯堡大学博士学位。吴文俊首先受陈省身的指导，从事拓扑学方面的研究。由于在拓扑学中的示性类及示嵌类突出成就，吴文俊被授予首届国家自然科学一等奖（同时获奖的人员为华罗庚以及钱学森）。1976年开始，吴文俊汲取了中国古代数学的精髓，开始了迈向数学机械化证明的全新征程。
初等几何的传统证明不是机械化的，从公理推到最后的结论往往需要借助灵感，比如证明者需要创造性地画上许多条辅助线，从而给证明者带来了很大麻烦。有没有可能通过算法机械化地对初等几何进行证明呢？塔尔斯基曾给出结论说一阶实数（初等几何和代数）是可判定的，这说明，找出算法对所有初等几何和代数问题给出证明是有可能做到的。
吴文俊通过研究中国古代数学史发现，中国古代数学虽然没有发展出希腊欧几里得公理化的演绎推理体系，却有非常好的实际应用效果，中国古代数学体系包含了高度实用的算法。我们知道算法是现代计算机的灵魂，机械化恰是其最大特点之一。1977年，吴文俊将中国数学思想运用到初等几何定理的判定上，提出了平面几何及微分几何的判定法,证明了初等几何主要一类定理的证明可以机械化。
其证明方法分为3个主要步骤。第一步, 从几何的公理系统出发, 引进数系统与坐标系统, 使任意几何定理的证明问题成为纯代数问题；第二步, 将几何定理假设部分的代数关系式进行整理, 然后依据确定步骤验证定理终结部分的代数关系是否可以从假设部分已整理成序的代数关系式中推出；第三步, 依据第二步中的确定步骤编成程序,并在计算机上实施, 以得出定理是否成立的最后结论。吴文俊给出的实现机器证明方法被称为“吴文俊消元法” 或“吴方法”。
吴文俊借鉴了王浩的说法，将这种用机器证明定理方法称为“数学机械化”，并在中国科学院开设了几何定理证明课程，中科院计算所的研究生周咸青旁听了吴文俊的课程，并拿到了吴文俊还未出版的《几何定理机器证明的基本原理》的手稿。后来，周咸青在美国德克萨斯大学奥斯汀分校留学，周咸青运用“吴方法”得出了一些研究成果，使得“吴方法”和吴文俊的名字出现在机器定理证明界，并引发关注。
吴文俊在数学所作报告（图片来源：http://www.amss.ac.cn/wwj/mtbd2017/index_4.html）
60岁开始学编程，20年不到获最高奖项
1979年，吴文俊的工作得到了杨振宁的关注，普林斯顿高等研究院邀请吴文俊访美，先后在普林斯顿高等研究院、加州大学伯克利分校以及王浩所在的洛克菲勒大学讲授中国数学史和机器定理证明。普林斯顿的听众没有表现出对机器定理证明的兴趣，但是在加州大学伯克利分校，著名数学家、菲尔茨奖得主斯梅尔（Steve Smale）高度评价了吴文俊的工作，令吴文俊感到欣慰，王浩也积极地将吴文俊的工作成果推向定理证明界的同行，最终使得“吴方法”在国际定理证明界引起重视。
在吴文俊访美的同一年，当时的中科院副院长李昌以及系统科学研究所关肇直院士为吴文俊申请到了两万五千美元的外汇到美国买了一台家用电脑，已经60岁高龄的他开始学习计算机编程语言，从BASIC语言开始，吴文俊在这台家用电脑上继续开展他的“数学机械化工作”，并取得了丰富的成果，他的“吴方法”也得到进一步发展。1997年，在周咸青的导师博耶尔（Robert Boyer）和华人计算机科学家项洁(Jie Hsiang)的提名下，吴文俊获得机器定理证明领域的最高奖项Herbrand奖，这是该奖项首次颁发给中国科学家。
吴文俊在电脑前工作（图片来源：中国科学院数学与系统科学研究院网站http://www.amss.cas.cn/wwj/yrxm/201705/t20170507_4784612.html）
吴文俊对于颁发给他的诸多荣誉，说过这样一句话：“对我个人而言，每次获奖都是高兴的事儿，但对一个国家的科学发展而言，稍做出成绩，就被大家捧成英雄，像朝圣一样，这个现象不是好事情，甚至可以说是坏事情，这说明我们的科研还在一个相对落后的阶段。要是在这一个领域，发现有十个八个研究人员的工作都非常好，无法判定谁是英雄，那才说明我们发展了，进步了。”
结语
许多研究数学的人知道，当前国际流行的主要符号计算软件都实现了中科院院士吴文俊的算法。可以说，吴文俊是我国科研整体水平较为落后的年代里，较少的为人类文明做出过重要贡献的中国人之一，他在机器定理证明方面的成就足以让他的名字写进人工智能发展的历史书里。同样，我们也可以认为，中国古代科学思想蕴藏着极大的价值，开发它对当今的科学技术发展仍然有重要的借鉴价值。
参考文献:
[1]尼克.人工智能简史[M]. 北京：人民邮电出版社，24-54.
[2]纪志刚.吴文俊与数学机械化[J].上海交通大学学报(社会科学版),2001(03):13-18
[3]傅海伦.定理机器证明思想的产生与发展[J].科技导报,2001(06):14-15+30.
[4]陆广地.吴文俊的贡献及其对数学发展的推动——深切悼念吴文俊院士[J].广西民族大学学报（自然科学版）,2017,23(2):20-23.
文章首发于科学大院，仅代表作者观点，不代表科学大院立场。转载请联系cas@cnic.cn。科学大院是中科院官方科普微平台，由中科院科学传播局主办、中国科普博览团队运营，致力于最新科研成果的深度解读、社会热点事件的科学发声。