用机器证题

张景中　彭翕成

初中同学中的“数学迷”们，谁不喜欢几何哩.

几何证题，变化万千.看起来似乎难以下手的一道题，只要在图上添上适当的辅助线，往往就云开雾散，妙趣横生.

正因为几何证题变化万千，所以也就不好做.难就难在看不出一般的规律.

例如，在△ABC中，已知AB = AC，∠ABC、∠ACB的平分线为BD、CE.求证BD = CE.如图1，这只要证明△DBC≌△ECB（ASA），问题便可迎刃而解.可是，把已知和求证交换一下，这一换，问题就难多了.

100多年前，德国数学家雷米欧司公开提出了这个问题.他说，几何题在没有证明出来之前，很难说它是难还是易.等腰三角形两底角的角平分线相等，初中学生都会证.可是反过来，已知三角形的两条角平分线相等，要证它是等腰三角形，可就不好证了.

后来，德国著名数学家史坦纳解决了这个问题，使它成为一个定理，叫做史坦纳-雷米欧司定理.

经过名人一做，这个问题也就出了名.有一个数学期刊还曾经公开征求这条定理的证明，收到了形形色色的证法.他们经过挑选和整理，得到了60多种证法，编印成了一本书.

到了20世纪60年代，有人用添圆弧的办法得到了一个十分简单的证法.从雷米欧司提出问题到找到这个简单的证法，竟过了100年之久.而且，人们找到了60多种证法，偏偏没有发现这个简单的证法.可见，几何证题的变化实在是太多了.

几何证题既然这么千变万化，人们自然会想：能不能找到一个固定的方法，不管什么几何题到手，都可以用这个方法一步一步地做下去，最后，或者证明它，或者否定它呢？

19至20世纪的大数学家希尔伯特证明：有一类几何题，可以用一种统一的方法，一步一步地得到最后解答.后来，数学家塔斯基证明：所有的初等几何命题，都可以用机械方法找到解答.可是，他的方法太复杂了，即便是使用高速电子计算机，也只能证明一些很平常的定理.

我国著名数学家吴文俊，提出了用机器证明几何定理的方法.他用到了我国古代的数学思想和方法.用这个方法，可以在计算机上证明许多相当复杂的定理，还能证明高等数学中许多微分几何的定理.

用机器证明几何定理，主要的思路是用坐标方法，把几何问题转化成代数问题来解决.要是你有志将来研究这方面的问题，从现在起就应该好好学习几何、代数和解析几何的基础知识了！