数学定理证明机械化的中国学派（II）

Posted 2020-09-26 llguanli

　所谓“学派”是指：存在一帮人，具有同样或接近的学术观点或学术立场，採用某种特定的“方法”（或途径），在一个学术方向上共同开展工作。而且做出了相当有迎影响的学术成就。

数学定理证明机械化的途径非常多，可是。“吴方法”仅仅有一种。什么是“吴方法”？我们拿初等（平面）几何学为例，所谓“吴方法”实质上就是“方程联立求证法”。

什么叫“方程联立求证法”呢？

比方说，我们须要求证一个几何“事实”（或断语）：三线“共点”。大家知道，初等平面几何里面有几百条“定理”须要证明。比方，三条直线“共点”，看起来这是显而易见的事情。可是，使用计算机自己主动证明这一事实却并不easy。

吴方法的第一步：实现“代数化”，即建立坐标系。把问题条件所有翻译成“代数方程式”（事项即“前提条件”），然后，把须要证明的事实也翻译成“代数方程式”（有待证明的事项）。吴方法的第二步：方程联立求证。

把前提条件（方承租）与待证明的方程“联立求解”，假设待证明的“方程”经过自己主动联立求解过程。变为一个恒等式，那么，这个恒等式就表示“全部前提条件”满足待证的“结论”，所以，定理得到证明，否则，问题无解。

在国际学术界，“吴方法”独树一帜，不随大流，效率最高，得到国际同仁赞扬与肯定。

经过多年人才积累，在数学定理证明机械化研究领域，研究业绩非凡，国内”吴氏学派“终于形成。请见：中科院数学机械化国家重点实验室官网。

袁萌　７月５日