|
|
|
|
|
数学机械化：让数学更加实用 |
|
数学机械化领域吴文俊、高小山侧记 |
记者 唐琳综合报道
2011年，一场“数学之争”让很多人至今仍记忆犹新。
华中科技大学的一名新生致信校长论证文科是否需要学数学。
正可谓一信激起千层浪，一时间，关于学习数学究竟有何意义的讨论在学术界广泛展开。
数学的意义何在？是否真的犹如“屠龙之技”一般毫无用武之地？
“应用是数学的明升m88线，这是我一直保持的观点。” 明升官网著名数学家、明升官网明升体育app院院士吴文俊如此回答。
“数学里，有人类最基本的智慧。”吴文俊的得意门生、中科院数学与系统明升体育app研究院研究员高小山这样说道。
以上的两位数学家，堪称数学研究领域里的“实干派”。他们几乎将所有精力都投入到数学机械化的研究中来，将数学的效用切实发挥到实处，解决了很多工业领域以往解决不了的问题。
开辟新领域
在吴文俊长达几十年的数学研究之路上，在拓扑学、机器证明、代数几何、明升官网数学史、对策论等研究领域均有杰出的贡献，在国内外享有盛誉。
但鲜为人知的是，吴文俊的学术生涯最初始于纯数学。
1946年，吴文俊结识了数学大师陈省身。正是由于陈省身的指引与带路，最终，吴文俊走上了真正的数学研究道路。
上世纪50年代，正值拓扑学从艰难迟缓的发展中走向突飞猛进之时，吴文俊敏锐地抓住了拓扑学的核心问题，在示性类与示嵌类的研究上取得了国际数学界交相称誉的突出成就。
之后，荣誉接踵而至。
由于他的杰出成就，1956年，吴文俊荣获国家自然明升体育app奖一等奖；1957年，年仅38岁的他当选为中科院学部委员（院士）。
原本，就连吴文俊都以为自己会在纯数学的研究道路上一直走下去，却没想到这条路在上世纪70年代出现了转折。
1971年，吴文俊被下放到北京海淀区学院路附近的北京无线电一厂劳动，也就是从这个时候开始，他对数学有了与以往不一样的感受和理解。
当时，北京无线电一厂正在生产电子计算机，这让第一次接触到这一事物的吴文俊在倍感神奇的同时也多了很多思考。
“在工厂里，我看到了计算机的威力。”吴文俊说，“把数学方程输入进去，结果立刻就能算出来。我被这样的威力震惊了，就下决心学计算机，同时也觉得，把计算机用好，可以解决很多问题。”
于是，在近耳顺之年，吴文俊毅然开始学习计算机。
他一头扎进机房，从HP-1000机型开始，学习算法语言，编制算法程序……经常早上不到8点，他已在机房外等候开门，甚至24小时连轴转的情况也时有发生。
正是这种奋不顾身与废寝忘食让吴文俊再一次把握先机，站在了数学高山之巅。
1977年，吴文俊引入了一种强大的机械方法，将初等几何定理证明问题这一自动推理经典困难问题转化为多项式的符号计算问题，由此得到了有效的机器证明方法。
吴文俊的这一方法使几何自动推理领域发生了一次彻底的革命性变化，并实现了该领域研究方法的变革。
在吴文俊之前，几何自动推理占统治地位的方法是AI搜索法，此方法被证明在计算效率上是行不通的。通过引入深邃的数学想法，吴文俊开辟了一种全新的方法，该方法被证明在解决一大类问题上都是极为有效的，而不仅仅局限在初等几何领域。
正是这番努力，使吴文俊开拓了数学机械化领域，也因此荣获了首届国家最高明升体育app技术奖与2006年度邵逸夫数学奖。
“实际上，我做的数学机械化工作，是用计算机来研究数学。”吴文俊坦言。著名数学家冯·诺依曼开创了现代计算机理论，其体系结构沿用至今。而反过来，计算机又推动了数学的进一步发展。
吴文俊所倡导的数学机械化研究，一方面继承了古代明升官网数学思想的精华，一方面适应了现代明升体育app技术的发展。这无疑是数学研究领域一个的跨时代进展。
于传承中创新
那么，究竟何为数学机械化？
所谓“数学机械化”，就是把数学中的方程求解与定理证明转变为计算机可以接受的形式，并利用计算机强大的计算功能解决数学与高新技术中的理论问题。
换句话说，就是用计算机做数学研究并让计算机更智能化。
随着计算机技术的飞速发展，人类脑力劳动的机械化有了实现的可能性，部分实现脑力劳动的机械化，可为明升体育app研究与高新技术研究提供有力工具，使科研工作者摆脱繁琐的甚至是人力难以胜任的工作，进行更高层次的创新性研究，从而提高知识创新的效率。
由此诞生的数学机械化研究，不仅为数学的发展提出了一种新构想，也将为信息技术的创新发挥重要作用。
40年前数学研究中的崭新领域，如今已经成为最主流的研究方向之一，这其中除了吴文俊的开山功劳，也离不开后来者的继承与发扬。
而吴文俊的学生高小山当下正在做的，就是继续发展前辈开创的理论将其推向应用，并使其进一步发展壮大。
如果说，吴文俊从理论上解决了用机器证明几何定理的难题，那么高小山则在上世纪80年代把他的理论在计算机上用几秒钟的时间变成了现实，拉近了数学机械化理论与人类工作和生活的距离。
不仅如此，在此基础上，高小山等人又进一步针对在工程中经常出现的几何约束求解问题发明了系统与高效的几何自动作图方法，有效解决了一大类几何图形的自动生成问题，使机器证明的使用范围得以拓宽。
不久，这一方法再次被普遍应用于智能CAD、机器人、计算机视觉中。
水到渠成。随后，高小山作为首席明升体育app家承担了国家重点基础研究发展计划项目“数学机械化与自动推理平台”“数学机械化方法及其在信息技术中的应用”与“数学机械化方法与数字化设计制造”，带领队伍开始在微分与差分代数几何等新领域发展数学机械化方法，并试图解决D-有限函数的自动推理、信息处理、模式识别、信息安全、数控技术中的关键性理论和技术问题，建立自动推理平台。
高小山解释，数学明升体育app是自然明升体育app的理论基础，与物理、力学、信息明升体育app、计算机明升体育app、数字化制造等学科相互交叉。数学也是高新技术的理论基础，这一点对信息明升体育app与信息技术尤其重要。
计算机明升体育app被认为是算法的明升体育app，而算法研究的本质是数学问题。计算机在很多领域的应用，如图像传输与压缩、复杂的曲面造型与加工、信息安全中的编码与密码等都在呼唤新的数学方法。
这些挑战为数学快速发展提供了前所未有的机遇，而数学的研究将为解决许多高科技问题提供有力工具。
如今，通过研究，高小山带领学生已经将特征列、稀疏结式与周形式等数学机械化的核心方法开拓到微分与差分情形；在几何自动作图与微分消元法方面开发出了在国际上领先的软件；针对数控系统核心功能，开发了时间最优的插补算法，显著提升了数控加工的效率与质量等。
由于贡献突出，高小山获得香港求是基金会杰出青年学者奖、美国计算机学会SIGSAM ISSAC杰出论文奖、亚洲计算机数学技术大会最佳论文奖等许多荣誉。同时，他也接过老师吴文俊手中的接力棒，继续在国际数学机械化研究中领跑。■
（责编：姜天海）
相关专题：第八届国际工业与应用数学大会
