数学定理证明机械化的中国学派(II)

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



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

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



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



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



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



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

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



袁萌 7月5日



原文地址:https://www.cnblogs.com/llguanli/p/7103068.html