用计算机软件验证和证明数学问题应谨慎

文/宁玉川

摘 要：计算机图形软件的算法也是基于数学理论建立起来的，由于程序员编写的程序所运用的数学原理是看不到的，因此一不小心，就会犯下循环论证的错误。

关键词：计算机证明；循环论证；过程目标

在初中数学教材（人教版）上，设置了几个可用计算机软件去验证的数学问题，如，探索旋转的性质、探索二次函数性质、探索位似性质等。这些内容的设置，丰富了教材的内容，增强了教材的趣味性，具有一定的时代特色。

但是，用计算机验证或证明数学问题真的具有合理性吗？

比如，在初中数学教材（人教版）九年级下册，第27章中的“平行线等分线段对应成比例”一节，课本上是通过让学生画图并测量得出结论的。然而，学生画图和测量不可能十分精确，都会出现误差，有的只能得出近似成比例的结果，这时，我们应该用归纳法得出猜想，再通过大量实验验证其合理性、真实性、可靠性。

如果某人试图用相似三角形的性质去证明上述定理，显然是十分荒谬的，显然这是犯了循环论证的错误。

也有的教师为了能完美地得出精确的实验结果，提出了用计算机软件测量验证的方法，甚至在一些公开课活动中，也动用了此方法。评课时，很多教师对此大加赞赏，说什么既减少了实验误差，又使用了现代教学手段。岂不知，不知不觉中，我们就有可能犯了一个严重的逻辑错误——循环论证。

为什么这样说呢？

因为计算机图形软件的算法也是基于数学理论建立起来的，各种应用软件都是用一些计算机高级语言程序开发的，这些高级语言为开发者提供了大量的函数（又称为类）模型，用于软件开发者综合使用这些函数处理各种信息，包括图形。而应用程序的使用者之所以移动鼠标就可以画出各种图形，是因为计算机通过应用软件把鼠标的坐标信息传递给了这些函数模型，从而画出（显示）了相应的图象。在高级语言提供的类函数中，包含了类似于平线线分线段成比例的类函数，这个类函数就是基于平行线分线段成比例建立起来的。我们应用计算机软件画出的三条平行线分两条直线一定是符合函数模型的，也就是说计算机是运用平行线分线段成比例计算出显示坐标，从而了画出的平行直线。如果我们又反过来用计算机建立的平行直线去验证所截线段是否成比

例，那恰好等同于用平行线分线段成比例本身去验证自己。所以说，用计算机软件证明上述定理是荒谬的，犯了循环论证的严重错误。

也许某些图形软件在处理有关平行线的绘图时没有使用类似于平线线分线段成比例的类函数，而使用的是与之不相关联的算法编写的应用程序。如果是这样的话，我们使用它去证明上述的平行线分线段成比例是没有问题的。可是我们不是应用程序的编写者，当然并不知道某个软件运行时，使用的是何种算法，因此盲目用计算机软件证明一个数学问题是不可靠的。

我们不要误认为计算是万能的，计算机是人类用已有的智慧建造出来的，在计算速度和记忆检索能力方面超过了自然人，但是这些能力毕竟是程序编制者赋予的，在计算方法方面永远按照编程者给出的指令去运行。编程者所提供给计算机的计算方法，无不来自已有的数学定理定律。到目前为止，还没听说过哪台计算机能自己编写真正意义的新的计算方法。一些原初的基本的定理，是不可能用计算机证明的。所谓计算机证明、验证，充其量只是一种旁证而已。也就是说，计算机只可以证明一些推论，验证一些推广，验证解答的正确性。所以说计算机证明只是一种辅助的验证，具有很大的局限性。

所谓的计算机计算证明，至少到现在为止，还处于初级的研究阶段。就拿最为著名的“用计算机证明四色定理”为例：20世纪初，肯普提出了一个证明的思路，不过过程十分繁杂。富兰克林于1939年证明了22国以下的地图都可以用四色着色。1950年以后，人们把定理的证明推广到35国地图。1960年又证明了39国以下的地图也可以，随后又推进到了50国。但是由于运算十分复杂，推进十分缓慢。直到1976年，美国数学家阿佩尔与哈肯把证明方法过程编写成程序输入了计算机，让这些复杂演算用计算机去完成，结果计算机用了1千多小时，做了100亿多个判断，终于完成了四色定理的证明，轰动了全世界。两位数学家谦虚地说是计算机完成了四色定理的证明。不过多数科学家并不赞同这是计算机取得的成就，因为这个证明的办法是数学家找到的，只是因计算量特别大，短时间内用纸笔很难完成，所以编写成程序输入计算机，计算机发挥了其计算速度快的特点，在一个相对较短的时间内，按照人所设定的流程，完成了繁杂的演算过程而已。至今人们还在寻找四色定理简洁明快的书面证明方法。

综上所述，计算机证明数学问题，至今仍处于探索研究阶段。我们在教学中不要轻言所谓用计算机去证明数学定理，不要误导学生，不要让他们误认为可以不用学习，什么事情都可以交给计算机，要让学生知道计算机也是听人的指挥的。

虽然用计算机去证明数学定理是不一定都是可行的，但是我们用它验证和解题倒是可以的，让它协助我们做一些复杂的演算也是可以的。初中教材中所提供的都是用计算机验证的方法，这种验证只是在一些局部的范围内具有合理性，所以不能乱用。由于程序员编写的程序所运用的数学原理你是看不到的，因此一不小心，我们在不知道的情况下就会犯下循环论证的错误。

参考文献：

孙熙椿.几何定理计算机证明［M］.科学出版社，2007-06-01.

编辑 韩 晓

endprint