证明正弦平方加余弦平方等于一

这个证明在初中几何课本就有。不一定用复杂的方法，不用推理机，从离散数学角度，就可以找到计算机证明的方法。如何做？

我们设计一个没有任何数学公式的程序，那里　给出证明该公式的预备条件：

（１）正弦等于对边Ａ比斜边Ｃ。………………………………（正弦定义）

（２）余弦等于邻边Ｂ比斜边Ｃ。………………………………（余弦定义）

（３）对边平方加邻边平方等于斜边平方。……………………（勾股定理）

（４）如Ｘ／Ｙ；Ｚ／Ｙ；则Ｘ／Ｙ＋Ｚ／Ｙ＝（Ｘ＋Ｚ）／Ｙ。……（通分）

（５）（Ｘ／Ｙ）＾２＝Ｘ＾２／Ｙ＾２。……………………（分数平方的展开）

（６）Ｘ／Ｘ＝１。………………………………………………（除法规则）

准备条件是证明中不可少的，我的这个程序简单，只给出必备条件。完善的证明程序，其条件会比所需条件多很多，这也就提高了选择必备条件的难度。

注意“……（）”是我用来说明程序的，不写进程序中。条件是要写进程序中的，对于程序来讲，它们只不过是一些字符串，程序对它们的含义并不理解，完成证明也不需要程序对公式理解。

求证：正弦平方加余弦平方＝？

程序运行要从求证出发，“求证”二字只是为了使程序找到出发点，也不要求程序的理解。对于程序来说，这两个字只是两个连接的字符。它以后的字符串（欲证之公式），才是程序找寻操作的依据。

程序里设置两个替代操作：

（１）等量替代：把等式左侧的用等式右侧的代替。

（２）假设量替代：把假设相等的东西，带入相关公式。

程序里还设置一个表达操作：把证明过程显示出来，再用一个等式把求证结果表达出来。

程序里还设置一个找寻操作：寻找相关等式的操作。

“等量替代操作”，是把完全相同的字符用等号后面的字符代替，程序在替代时完全不理解字符的含义。“假设量替代操作”，它比较复杂，首先它需要识别（但不必理解）等号和运算符号，把运算符号隔开的字符串作为操作对象。完成假设时，把某一个单字符对象用等号与其它公式的操作对象连接。然后用等量替代操作，进行替代。

找寻操作，就是先把求证的某一操作对象，在准备条件中检索该字符串，发现它的位置，就进入替代操作。如果准备条件多于必备条件，有些检索到的结果可能是无用的，下面的工作就会无法进行，此时要放弃检索到的公式。继续寻找。这个过程也叫做“尝试错误”过程。在离散法模拟思维时，尝试错误过程是不可少的。但是，本程序由于只有必备条件，不必经历尝试错误过程。

表达操作，就是把证明每步结果显示出来，中间过程（例如尝试错误过程）则不显示。这些作用在编程时要考虑进去。

 先按上述要求编写程序，然后就运行程序。程序的运行情况大体是这样：

程序从求证项出发，进行找寻操作，在预备条件里找寻相关等式。先找到（１），用等量替代操作把它代入求证项的相关位置。然后找到（２），用等量替代操作把它也代入求证项的相关位置。得到（表达操作）：

　　（Ａ／Ｃ）＾２＋（Ｂ／Ｃ）＾２＝？

然后继续进行找寻操作。找到（５），用假设量（设Ｘ＝Ａ／Ｃ；Ｙ＝Ｂ／Ｃ）替代操作，代入后得到（表达操作）：

　　Ａ＾２／Ｃ＾２＋Ｂ＾２／Ｃ＾２＝？

然后继续进行找寻操作。找到（４），用假设量（设Ｘ＝Ａ＾２／Ｃ＾２；Ｙ＝Ｂ＾２／Ｃ＾２）替代操作，代入后得到（表达操作）：

　　（Ａ＾２＋Ｂ＾２）／Ｃ＾２＝？

然后继续进行找寻操作。找到（３），用等量替代操作，代入后得到（表达操作）：

　　Ｃ＾２／Ｃ＾２＝？

然后继续进行找寻操作。找到（６），用假设量（设Ｘ＝Ｃ＾２）替代操作，代入后得到（表达操作）：

　　Ｃ＾２／Ｃ＾２＝１

最后，用假设量（设？＝１）替代操作把结果代入求证，得到（表达操作）：

    正弦平方＋余弦平方＝１

以上运行过程的一段段语言部分，是程序操作过程，屏幕不显示。“得到（表达操作）：”后面的公式在屏幕上显示，其为程序证明过程的真实写照。

我给出的证明正弦平方加余弦平方等于１的程序。依靠三个主要操作（找寻操作、等量替代操作、假设量替代操作），用离散的方式，还可以证明很多数学上的公式、定理。它虽然还不那么智力高超，但是它的智力应该比连续数学的各种模型高。

值得注意的是，在这个程序中我们没有用数学方法构造程序，什么加权平均、权重、调和函数都靠边站。只用到三个操作：找寻操作、等量替代操作和假设量替代操作。我把这种不用高等数学唬人的编程理念，叫做图灵主义。