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

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

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

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

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

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

在国际学术界,“吴方法”独树一帜,不随大流,效率最高,得到国际同仁赞扬与肯定。经过多年人才积累,在数学定理证明机械化研究领域,研究业绩非凡,国内”吴氏学派“最终形成。请见:中科院数学机械化国家重点实验室官网。

袁萌 7月5日

版权声明:本文为博主原创文章,未经博主允许不得转载。

心有多大,舞台就有多大。

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

相关文章:

你感兴趣的文章:

标签云: