2011年，一场“数学之争”让很多人至今仍记忆犹新。华中科技大学的一名新生致信校长论证文科是否需要学数学。正可谓一信激起千层浪，一时间，关于学习数学究竟有何意义的讨论在学术界广泛展开。
数学的意义何在？是否真的犹如“屠龙之技”一般毫无用武之地？“应用是数学的生命线，这是我一直保持的观点。”中国著名数学家、中国科学院院士吴文俊如此回答。
“数学里，有人类最基本的智慧。”吴文俊的得意门生、中科院数学与系统科学研究院研究员高小山这样说道。
导语
思维是人类智能的核心，逻辑思维作为思维的高级形式，人们很早就开始了对它的探索。古希腊哲学家亚里士多德在中世纪就创立了形式逻辑学，其三段论至今仍是我们写作的利器。我国春秋战国时期公孙策的“白马说”、墨子的“墨经”等则构成了中国古代逻辑思想的精髓。随着生产力的发展，自然科学的进步，数学方法的广泛应用，17世纪诞生了数理逻辑这门学科。
德国数学家莱布尼茨（GottfriedWilhelmLeibniz）作为数理逻辑的奠基人，他继承了思维可以计算的思想，把人类推理归纳为某类运算，首次提出“通用符号”和“推理计算”等概念，被看作是对“机器思维”的初步探索者。
1960年，华裔美国数理逻辑家王浩提出命题逻辑的机器定理证明的新算法，用计算机证明了集合论中的300多条定理。1965年，美国科学家鲁宾逊（JohnAlanRobinson）提出词逻辑的“消解原理”，简化了判定步骤。1977年，我国数学家吴文俊提出了初等几何判定问题的机器定理证明方法，并推广到初等微分几何、非欧几何领域。
吴文俊的自动机理论
在吴文俊长达几十年的数学研究之路上，在拓扑学、机器证明、代数几何、中国数学史、对策论等研究领域均有杰出的贡献，在国内外享有盛誉。
1977年，吴文俊引入了一种强大的机械方法，将初等几何定理证明问题这一自动推理经典困难问题转化为多项式的符号计算问题，由此得到了有效的机器证明方法。吴文俊的这一方法使几何自动推理领域发生了一次彻底的革命性变化，并实现了该领域研究方法的变革。在吴文俊之前，几何自动推理占统治地位的方法是AI搜索法，此方法被证明在计算效率上是行不通的。
通过引入深邃的数学想法，吴文俊开辟了一种全新的方法，该方法被证明在解决一大类问题上都是极为有效的，而不仅仅局限在初等几何领域。正是这番努力，使吴文俊开拓了数学机械化领域，也因此荣获了首届国家最高科学技术奖与2006年度邵逸夫数学奖。“实际上，我做的数学机械化工作，是用计算机来研究数学。”吴文俊坦言。著名数学家冯·诺依曼开创了现代计算机理论，其体系结构沿用至今。而反过来，计算机又推动了数学的进一步发展。吴文俊所倡导的数学机械化研究，一方面继承了古代中国数学思想的精华，一方面适应了现代科学技术的发展。这无疑是数学研究领域一个的跨时代进展。
中国人工智能学会在2010年设立“吴文俊人工智能科学技术奖”，这是一件有历史意义的战略举措。多年来，通过该奖项的颁发，让我们鉴赏着、见证着中国人工智能领域取得的成果和人工智能事业发展的蓬勃态势。
何为数学机械化？
所谓“数学机械化”，就是把数学中的方程求解与定理证明转变为计算机可以接受的形式，并利用计算机强大的计算功能解决数学与高新技术中的理论问题。
换句话说，就是用计算机做数学研究并让计算机更智能化。
随着计算机技术的飞速发展，人类脑力劳动的机械化有了实现的可能性，部分实现脑力劳动的机械化，可为科学研究与高新技术研究提供有力工具，使科研工作者摆脱繁琐的甚至是人力难以胜任的工作，进行更高层次的创新性研究，从而提高知识创新的效率。
由此诞生的数学机械化研究，不仅为数学的发展提出了一种新构想，也将为信息技术的创新发挥重要作用。
吴文俊院士由于对数学机械化研究的突出贡献，获得首届国家最高科学技术奖时，我们看看当时评委给与他的颁奖词，我们从中能看到学机械化的独特魅力。
40年前数学研究中的崭新领域，如今已经成为最主流的研究方向之一，这其中除了吴文俊的开山功劳，也离不开后来者的继承与发扬。
自1976年冬，吴文俊在中国古代数学机械化思想的启发下，尚不知外国人的研究成果，独辟蹊径，大胆地投入数学机械化的研究，创建了数学机械化方法：从几何公理体系出发，引进坐标，将任意几何问题代数化→将证明题的假设与结论分别表示成多元多项式方程→在电子计算机上运算，以判断定理是否成立。
吴文俊完成了西姆森线、费尔巴哈定理、毛莱定理等一系列初等几何的证明。随后，他又把证明的范围扩大到非欧几何、仿射几何、圆几何、线几何、球几何等领域。
中国数学家吴文俊，终于实现了千百年来几何定理机械化证明的梦想。被誉为“吴方法”的诞生，给两千多年的公理化演绎体系带来了强烈冲击。
吴文俊教授还用自己的方法，证明了可以用计算机程序从刻卜勒定律推导出牛顿定律，这已超出了数学定理机械化证明的范畴，而是属于更广的自动推理。
而吴文俊的学生高小山当下正在做的，就是继续发展前辈开创的理论将其推向应用，并使其进一步发展壮大。如今，通过研究，高小山带领学生已经将特征列、稀疏结式与周形式等数学机械化的核心方法开拓到微分与差分情形；在几何自动作图与微分消元法方面开发出了在国际上领先的软件；针对数控系统核心功能，开发了时间最优的插补算法，显著提升了数控加工的效率与质量等。
由于贡献突出，高小山获得香港求是基金会杰出青年学者奖、美国计算机学会SIGSAMISSAC杰出论文奖、亚洲计算机数学技术大会最佳论文奖等许多荣誉。同时，他也接过老师吴文俊手中的接力棒，继续在国际数学机械化研究中领跑。
结语
笔者认为，中国数学传统都是以算法为中心发展的，并且是以把几何问题化为代数问题求解为其特征的。中国数学家吴文俊院士将中国传统数学的构造性和几何代数化方法用于定理的机器证明获得成功。他的思路是把几何问题化为代数方程组，以整序原理消元求解，从而判断定理的成立与否。定理机器证明的吴文俊原理和求解高次联立程组吴文俊消元法的创立，已使我国在机械化数学领域处于领先地位，亦表明中国传统数学范式的新生。
参考文献：
中国科学院数学与系统科学研究院，数学机械化：让数学更加实用数学机械化领域吴文俊、高小山侧记
