最近在博客讨论中涉及到元数学、平面几何公理系统、多元多项式方程组的相容性判定与求根等问题。这些，使我联想到我的同学丁孙荭的相关研究。

丁孙荭和我都是秦元勋教授文革后招收的首批研究生，开始的研究方向都是相对论，后来根据他的情况改为专攻微分方程定性理论。在读研（硕士）期间，他已获得出色的研究成果，发表在《中国科学》（丁孙荭，Liénard 方程在有限区间上极限环的唯n性定理，中国科学，A辑，9（1982），792-800）。

在读研期间，秦元勋先生根据其在二机部九院工作的切身体会（参考《数学家秦元勋的传奇人生和主要学术成就》，《由自然与美谈起》），积极倡导在数学研究中使用计算机。1979年秦先生主导用计算机进行符号运算、实现了二次微分系统中心焦点判别公式的推导，发现前苏联科学院院士巴乌金的著名结果有一个关键性符号错误，首次得到正确的全部参数的二次微分方程系统的判据（Qin Yuanxun and Liu Zunquan, Mechanical deductionsof formulas of differential equations, (III) Kexue Tongbao, Vol.26, No.5, 1981,385-389）。就我所知，这是我国第一个利用机器证明的方法解决重要数学问题的成果。秦先生的表率，对我们研究生影响深远。

在拿到硕士学位后，由于丁的家在四川，尽管已获得很好的研究成果，那时也很难留在北京。所以，秦先生不舍地将他介绍到中科院成都分院数理科学研究室工作。在那之后，我们联系较少（上世纪八十年代的主要联系方式是通过平信）。但不断有些消息说成都分院要精简、改制，要求从事数学理论研究的转向从事应用研究。后来，大约在九十年代，又听说他被调离分院，到该院附属的从事计算机应用研究、开发公司工作，由科研编制变到企业编制。

2002年年底，我们在北京相聚，了解到他在成都分院及后来的公司工作中，做了一项极有意义的研究工作：平面几何的人工智能机器证明。

众所周知，平面几何问题的研究有两种方法：一种是经典的，通过公理体系，进行逻辑推理证明新的定理，做图，计算等。另一种方法是将平面几何问题化成解析几何问题，把几何问题转换成多元多项式方程组的相容性判定与求解问题。关于平面几何机器证明的研究大多基于后一种方法。

多元多项式方程组的相容性判定与求解是一个很复杂的问题。代数学经典名著， Algebra I-II（VanDer Waerden著），对相关的消元法有系统介绍。但在实际应用时，特别是变元多、次数高时，计算量极大，即使用计算机往往也难完成。我国吴文俊院士较早就系统研究解决办法，创造出很有成效的著名吴消元法（简称吴方法），该方法已用到平面几何问题的研究上。

后来，杨路教授，张景中院士等也给出了关于非线性代数方程组较好的算法（杨路,张景中,侯晓荣.非线性代数方程组与定理机器证明.上海:上海科技教育出版社，1996）。

特别要提到，九十年代，张景中还在美国维奇塔大学进行合作研究，出版以消点法为主题的英文专著《几何中的机器证明》。他吸取美国优秀教学软件《几何画板》的长处，给原有软件增加了大量新功能。2002年，数学软件《(Z+Z智能教育平台——超级画板》诞生了，取名“Z+Z”。

值得一提的是，张景中、杨路也是在成都分院数理科学研究室工作，张景中还一度任该室主任，他们都比丁孙荭资格老。毫无疑问，他们的研究肯定会对丁孙荭的研究带来积极影响。

果然，就在张景中等取得上述辉煌成果的同一时期，丁孙荭则另辟蹊径，不是将平面几何问题转化成解析几何问题，而是将经典、传统的平面几何证明的人类智能推理方式转化到计算机实现（即本文所提到的“平面几何的人工智能机器证明”），研制出了《嘉科平面几何》智能教育软件。该软件突破性地，应用人工智能推理数据库技术生成，在推理过程中能智能地添加辅助线、自动显示图形和相应的数值动态变化、能进行逆向推理等。那时，他已主持一个小公司“成都嘉科数码科技发展有限责任公司”。

该软件在2002年3月通过了中国教育部中央电化教育馆组织的，以清华大学严蔚敏教授为首的（7人）专家鉴定组的鉴定。图1，2 分别是鉴定证书与具体意见。

               图 1

                             图 2

由于丁孙荭的公司是企业，必须自谋生路。除做一些其它应用开发工作外，他将该软件制成光盘作为教育软件在市场上销售。好在，他的工作得到了一位慷慨的投资者的经费支持。

了解丁孙荭的软件后，我和我爱人感到他做了件相当了不起的工作。特别，我们都从事过中学教学多年，我爱人还多年担任平面几何的教学工作，所以有兴趣检验他的软件。我们反复检验、使用该软件，并比较其它软件（包括“Z+Z”），发现其功能确如鉴定书所述“架构先进、技术含量高、功能齐全、实用性好”。比起其它软件，我们觉得该软件绝对不差，但它更容易使用，而且在智能上（例如做辅助线）更具独创性。

我们也曾设法帮助销售该软件。但，那时中学已不把平面几何当作必修课，一些学校干脆取消了该课程，有的学校则消减了内容。普通人和学生家长都对平面几何失去兴趣，市场上几乎没什么人问津这类软件（可能也包括“Z+Z”）。经历这些困难，再加上已近退休年龄（他比我小一岁），丁孙荭将精力放在维持公司的生存，从事一些其它开发、应用工作。我们之间的联系变得越来越少。

正如本文开始所述，由于近期的讨论使我联想到丁孙荭的研究。由于我不是从事人工智能研究的，无法判断他的工作的意义大小。但有一个强烈感觉，他的研究是有特色、并十分出色的，不应因为有其他人不同方法的光辉成果而被视而不见、被埋没。

希望他能亲自介绍他的工作，并望有年轻人继承这一研究。