3. 数学定理的计算机证明
数学定理的计算机证明，又称机器证明，有广义和狭义之说。
广义之说是，数学定理的机器证明，顾名思义，就是通过机器的有限步推断完成一般数学定理的证明，简称为机器证明，又称为机械化证明、自动证明，因计算机是实现这类证明的最好机器，甚至也可以说是现在唯一真正可用的机器，所以常称为计算机证明；狭义之说是，把数学的某一类命题（数量可很多）从整体上加以考虑，建立统一的、确定的证明程序，经计算机有限步推断给出数学命题真假的证明,真者就成为定理。
从广义上讲，如四色定理、费马大定理等在计算机上进行的证明，应属于数学定理计算机证明的；但这类证明，一事一例，独具特点，不是对一类数学定理的证明，因此，从狭义上讲，它们并不属于数学定理的计算机证明。
数学定理的计算机证明是现代数学中一个新兴的边缘性学科，也是现代人工智能发展的一个重要方向，以下均简称为机器证明或计算机证明。从传统的定理手工证明到定理计算机证明，是现代数学思想方法的一次重大突破，既是计算机和人工智能发展的产物，也是数学自身发展的需要。
4. 计算机证明的可行性
西方的几何学是由欧几里德建立的一套公理化系统发展起来的，是按照定义——公理——定理——证明的演绎系统进行的。显然，这种公理化体系的几何定理证明现在还很难实现机械化。由于几何在数学中的历史地位及在数学教育中的重要作用，对几何定理进行计算机证明成了这一领域中的研究重点。
如何利用机器进行自动推理，特别是进行几何定理的自动证明，是西方学术界长期以来试图研究解决的问题。事实上，17世纪大数学家莱布尼兹就有机械化证明的设想；直到19世纪末，由于希尔伯特（David Hilbert）及其追随者建立并发展了数理逻辑，这一问题才有了明确的数学形式；又由于20世纪40年代计算机的出现，才使这一设想有了实现的可能和条件。
历史上一些大师级的数学家，曾在几何定理计算机证明这条路上进行过艰苦的探索。
为了用统一的方法处理千变万化的几何问题，笛卡尔（Ren Descartes）发明了坐标方法，创立了解析几何。跨19世纪、20世纪的大数学家希尔伯特，在它的名著《几何基础》中，曾给出了一类几何问题的机械化解题方法。电子计算机的出现，大大加快了数学定理计算机证明研究的进程，促进了几何问题求解的计算机证明研究。
1948年，塔斯基（Alfred Tarski）发表了一条引人注目的定理：“一切初等几何和初等代数命题构成的命题类，是可判定的”。这里，所谓“命题”是一个具有前提和结论的判断句；如果命题的前提和结论都可以用有限个整系数多项式的等式或不等式表达，就叫做初等几何和初等代数命题。如果有一套机械的方法，对于某个命题类的任一个命题，都能用这套方法经有限步的操作确定命题的真假，就说这个命题类是“可判定的”。

波兰裔犹太逻辑学家、数学家、语言哲学家阿 塔斯基 (1901–1983)

塔斯基的方法，先利用笛卡尔坐标把几何问题化为代数问题，再用代数方法来解决问题。沿这条路线，发展了几何问题计算机证明的代数方法。
1975年，考林斯（Collins）提出“柱面代数分解方法”，比塔斯基的方法效率提高了很多，但在计算机上仍只能解决个别稍有难点的几何问题。
笛卡尔——塔斯基——考林斯，这是用代数方法寻求几何问题机械求解的一条线。
另一条路线，是企图把解决几何问题的传统综合方法机械化，通常叫做后推搜索法，又提出了更有效的前推搜索法。这类方法，由于搜索空间过大等问题，未能形成有效的算法。
计算机早期只会进行单一的数值计算，到了20世纪60年代中，用它能做符号计算，有理式的四则运算，多项式的因式分解，求最小公倍式和最大公因式，甚至还能计算符号微积分，为几何问题的计算机证明提供了强有力的工具。
1977年，我国著名数学家吴文俊院士在《中国科学》杂志上发表了论文“初等几何判定问题与机械化证明”，提出了一个证明等式型初等几何定理的新的代数方法。1984年，中国留美学者周咸青在他的博士论文中把这个方法叫做“吴方法”，并列出了基于吴方法所编写的程序证明的130个几何定理。不久，他又在一本专著中列出了用吴方法证明的512个几何定理。吴方法从此在国际自动推理研究领域广为传播。
1984年，吴文俊院士的学术专著《几何定理计算机证明的基本原理（初等几何部分）》出版。这本专著遵循机械化思想引进数系和公理，依照机械化观点系统地分析了各类几何体系，诸如帕斯卡几何（Pascal's theorem），垂直几何，度量几何，欧氏几何等，证明确立了各类几何的机械化定理，系统地阐明了几何定理机械化证明代数方法的基本原理。

《几何定理机器证明的基本原理》一书

1992年，张景中院士和周咸青博士合作研究，提出了以面积法为工具，用计算机生成几何定理“短证明”的设想。这项工作被自动推理领域的国际同行誉为“计算机发展几何问题解题能力道路上的里程碑”，“自动推理领域30年来最重要的工作”。
1993年，张景中、杨路、高小山和周咸青等人把消点法推广到了非欧几何，用计算机发现了几十条非欧几何的新定理，并且自动生成了它们的可读证明。
迄今，人们已经用计算机证明了上百条重要的数学定理，甚至还曾经用计算机发现过一些猜想。
5. 计算机证明的应用
目前，计算机证明作为数学研究的一种方法，还存在着许多理论和技术上的问题，这些问题的解决将有待于算法理论、计算机科学和人工智能等各个领域出现新的重大突破。
近30多年来，数学定理计算机证明的研究从基础研究领域扩展到了应用研究和开发研究领域。这里所说的应用既有间接的，也有直接的。
在研究几何定理计算机证明时，创造或发展了一些新的方法或代数工具，它们可以用来解决其他领域的问题，如机构设计、曲面造型、计算机辅助设计、机器人控制、计算机视觉以及其他有关的数学问题，这是间接应用。
把几何定理机器求解的程序发展为软件，或者嵌入计算机应用软件，这是直接的应用。这类应用的实际需求，主要有两个方面：一是为研究者、教师和数学爱好者提供智能性几何解题电子词典，对两千多年的初等几何作一个相对完美的总结；二是应用几何定理机器求解研究的成果，可以研制出高智能的教育软件。
通过计算机证明，解决了数学中的百年难题，如四色猜想、费马大定理等，开阔了人类的视野，为数学发展开辟了一条新途径，意义重大，也是计算机证明的又一直接应用。
计算机证明同样有导致发现的功能，其中一个较为典型的例子是分形几何的创立。早在20世纪20年代，法国数学家朱利亚（Gaston Julia）就开始着手研究分形几何，但是由于这种几何图形的惊人复杂性，朱利亚的研究沉寂了几十年。直到60年代以后，美国数学家曼德勃罗 ( B.Mandelbrot )开始用计算机来画图，才使分形几何得到了真正的发展。

分形几何图形一例

社会的需求还会把机器求解的研究推向更广的领域，不仅研究几何问题的机器求解，而且要探讨一般理科问题的机器求解方法。