几何定理的机器证明

张景中　彭翕成

几千年来，人们解几何题的招数，层出不穷，争奇斗艳，概括起来，不外这4类：检验、搜索、归约和转换，50多年来，数学家和计算机科学家费尽心思，循循善诱，把个中奥秘向计算机传授，使得计算机解几何题的能力日新月异，大放光彩，除了灵机一动加辅助线，或千变万化的问题转换之外，前3种方法计算机都学得十分出色了，用机器帮助，以至在某种程度上代替学者研究几何，帮助乃至代替老师指导学生学习几何，已经从古老的梦想变为现实。

在几何定理机器证明中，采用代数方法，引进坐标，将几何定理的叙述用代数方程的形式重新表达，证明问题就转化成判定是否能从假设的代数方程推出结论的代数方程的问题，这样把几何问题代数化，自笛卡尔以来已是老生常谈，并无实质困难，然而代数化的过程，坐标点的选取和方程引进的次序都可能影响到后续证明的难度，甚至由于技术条件的限制，影响到证明是否可能完成，也就是说，几何问题化成纯代数问题之后，也并不见得一定容易，更不能说就能实现机械化了，这不仅是因为解决这些代数问题的计算量往往过大，令人望而却步，还因代表几何关系而出现的那些代数等式或不等式常常杂乱无章，使人手足无措，从这些杂乱无章的代数关系式中要找出一条途径，以达到所要证的结论，往往要用到高度的技巧，换句话说，即使你不怕计算，会用计算机来算，也不知道从何算起。

解几何题是思维的体操，是十分有吸引力的智力活动之一，图形的直观简明，推理的曲折严谨，思路的新颖巧妙，常给人以美的享受，许多青少年数学爱好者，往往首先是对几何有了浓厚的兴趣，用计算机证明几何问题，如果仅限于用平凡而繁琐的数值计算代替巧妙而难于入手的综合推理，则未免大煞风景，通过计算机的大量计算判断命题为真，确实是证明了定理，这是有严谨理论基础的，但这样的证明写出来只是一大堆令人眼花缭乱的算式、数字或符号，既没有直观的几何意义，又难于理解和检验，这跟几何教科书上十行八行就说得明明白白的传统风格的证明大相径庭，如果计算机给出的这一堆难于理解和检验的数据也算是几何问题的解答，这种解答只能叫做不可读的解答。

所幸的是，计算机不仅能计算，也能推理，只要我们会教，它也能学会传统风格的几何解题方法，我们希望的是，既要用计算机帮助人脑，减轻人的高级脑力劳动，还要在提高效率的同时，寻求保持传统几何的魅力。