符号主义和连接主义是人工智能方法的两大流派。历史上，作为连接主义的代表，人工神经网络几经沉浮，目前攀上了发展的巅峰，高歌猛进、如火如荼；而符号主义发展的巅峰之一，是吴文俊先生开创的机器定理证明。
吴先生曾经指出，源自希腊的西方数学主要遵循“公理化”的原则来搭建理论大厦；而中国古代数学的传统却着重于构造性算法化的证明，因而适合现代计算机科学发展的脉络。
公理化系统首先建立一系列“不可辩驳”的公理(axioms)，然后通过逻辑演算来推演引理、定理和推论，从而推演出整个理论体系。只要承认公理，那么所有的推导结果必然自动为真。特别是所有的推演过程都可以严格检验，由机械完成。数千年来，公理化方法已经成为各门科学发展的范式，从欧几里得几何，到牛顿力学，再到广义相对论。在数学的所有分支几乎都是以公理化系统为历史总结，成为这一分支成熟的标志，例如同调论(homology Theory)。饶有兴味的是，在数学中许多艰深的概念由于过于抽象，无法直接描述，反而以更为抽象的公理化方法来加以定义，比如Milnor介绍矢量丛的Stiefel-Whitney示性类的概念就是用如此手法，然后又异常迂回曲折地构造了一个真正的实例。
历史上，以希尔伯特(Hilbert)为代表的数学家力图用公理化方法来统一整个数学，建立一个包罗万象的公理系统，来囊括所有的数学真理。哥德尔的不完备性定理否定了这一宏伟蓝图。哥德尔证明任意一个包含初等数论的公理系统，并且是自洽的，它必定包含某些命题，这些命题的真伪无法被该系统证明；如果此系统无矛盾，则其无矛盾性不可能在此系统内证明。这意味着，对于任意包含有限公理的形式系统，存在一条数学真理，此系统可以表述但是无法证明，因此真理的探索过程是无止境的；同时，这一系统的无矛盾性，必须由其他系统来证明。这种现象比比皆是，例如某一数学领域最为根本的定理，往往用另外数学领域的方法来证明，代数的基本定理是说多项式方程存在根，这一定理只能用拓扑方法来证明。
欧几里得几何的公理体系不包含初等数论，它是完备的。长期以来，人类经过大量的生产实践，都认为欧几里得几何的几条公理不证自明，是唯一“真实”的几何。后来，罗巴切夫斯基将第五公设“过直线外一点存在一条平行线”修改成“过直线外一点存在无穷多条平行线”，通过逻辑演绎，建立了双曲几何。如果将此公设改成“过直线外一点不存在平行线”，则可以得到球面几何。长期以来，人们一直将双曲几何和球面几何作为纯粹智力游戏的产物，倾向于认为它们没有真实的物理基础。依随科学的发展，欧氏几何、球面几何和双曲几何都成为黎曼几何的特例，广义相对论的建立使人们相信黎曼几何物理真实性，从而不再纠结逻辑演绎结论的物理基础。历史的发展总是依循“否定之否定”的规律，共形几何的发展揭示了所有的二维黎曼流形，在保角变换下都可以归结为球面几何、欧氏几何和双曲几何中的一种，如图1所示。近些年来，依随计算机科学的发展，几乎所有的曲面几何计算问题都可以归结在这些标准空间中的计算问题，因此对于这三种古老而“正统”的几何研究日益复苏。
吴文俊先生为了弘扬中国数学构造性算法化的传统，将数学(特别是代数几何)与计算机科学相结合，开创了机器几何定理证明的方向，只手擎天地推动了数学机械化的发展。吴先生认为在很大程度上，人们可以用复杂的计算推演来代替抽象的推理，从而用计算机来辅助数学家去发现自然结构、获取数学真理。吴先生发明的吴方法，完全可以证明所有欧几里得几何的定理，同时被广泛应用于许多数学和工程领域。
机器几何定理证明
基于吴方法的自动几何定理定理证明大致步骤如下：
3. 用三角列中的多项式伪除结论多项式，如果余式非0，则我们说命题不成立；
4. 检查非退化条件，如果非退化条件满足(所有初式的乘积非零)，则我们说结论多项式由条件多项式生成。
我们可以用吴方法来证明结论多项式可以由条件多项式推出，从而证明了垂心定理。很多时候，机器给出的证明非常出人意料，更为简洁巧妙。
机器人路径规划
吴方法可以用来求解多项式方程组。
图3.机械臂逆向运动学。
在机器人应用中，机器人通过三维扫描获得物体的三维几何位置信息，从而得到最终机械手的位置和朝向，通过反解各个关节的旋转角度，和机械臂的伸缩，使得机械手达到目标位置，从而可以实现抓取。这被称为是逆向运动学问题(inverse kinematics)，需要求解多项式方程组，而吴方法正是解多项式方程组的有力武器。
数控机床
图4.五轴联动数控机床(5-Axis CNC Machine)。
在机械制造、机械加工领域，虽然3D打印技术突飞猛进，但是对于金属机械部件的制造加工主要还是依赖于数控机床(Computer Numerical Control Machine)。如果加工器件的几何形状复杂，需要用到五轴联动的数控机床，如图3所示。在数控技术中，机械零件一般用分片有理多项式来表示(NURBS)，加工刀具的轨迹和零件在空中的运动轨迹需要精确配合，以达到加工精度要求。这里，零件的表面是代数曲面，曲面上的轨线是代数曲线。加工时转头尽量垂直于曲面，同时控制运行速度和加数度，以及刀具施加的力量。如果加速度过大，有可能直接损坏刀具或零件。这里，需要求解大量的多项式方程组，吴方法在这个领域中大显神威。
计算机图形学
图5.光线跟踪法渲染的犹他壶。(Ray Tracing Utah Teapot)
在计算机图形学中，光线跟踪法(Ray Tracing)提供了高质量真实感绘制效果，因而在电影动漫中被广泛应用。许多曲面被表示成带参数的样条曲面(Spline Surface)，即为分片多项式或者有理多项式，其一般表示形式为
计算机视学
在计算机图形学和计算机视觉中，形状分析(shape analysis)是一个基本问题。形状的整体对称性是一个重要的指标，近些年来曾经引发过研究热潮。
这种变换被称为是对合变换(involution)，这种曲面被称为是超椭圆曲面(hyper-elliptic)。所有亏格为二的封闭曲面，嵌在三维欧氏空间之中，都是超椭圆的。那么，如何计算对合映射呢？
在标准度量(双曲度量)下，如果一条测地线都把曲面分割成多个联通分支，则此测地线必然经过Weierstrass point。
图中，曲面被分解成两个部分，对合映射将一部分映到另外一个部分。吴方法给出了计算曲面共形对称群的方法。
总结:
我们看到，吴方法提供了非常基本的算法，能够求解多项式方程组，证明初等几何定理，计算机器人路径规划，生成数控机床加工方案，进行参数样条曲面隐式化，求解代数几何问题等等，从而广泛应用于纯粹数学、计算数学以及众多工程领域。
吴方法为人工智能的符号计算提供了坚实的理论基础和高效的算法，特别是算法的每一步骤都可以被人类透彻理解，它代表了智能中严密清晰的逻辑思维层面，和连接主义中概率模糊的感性直觉层面互补。我们相信，在未来，吴方法必将在人工智能领域再放异彩。吴文俊先生的光辉思想将会被后人深入挖掘，继承发扬，彪炳千秋！
注：文章内的所有配图皆为网络转载图片，侵权即删！
吴文俊应用计算机进行几何定理的证明 吴文俊先生的吴方法怎么用？如何用吴方法证明几何定理？...
