2001年2月19日，中华人民共和国国家科学技术奖颁奖大会在北京人民大会堂隆重举行，当时的国家主席江泽民亲自为荣获国家科学技术奖的科学家发奖。荣获这一届国家科学技术奖的两位著名科学家之一就是吴文俊。他是因为在几何定理的机器证明方面的科研成果而获该年度国家科学技术奖的。

计算机作为数值计算工具的发明要归功于15世纪法国著名数学家、物理学家和思想家帕斯卡。帕斯卡在1644年制造的“加法机”是计算工具史上的一个里程碑，因为它包含着后来计算机的基本原理，为后来机械计算机的制造迈出了开拓性的一步。他自己在«沉思录»中也认为，计算器所进行的工作，比动物的行为，更接近人类的思维。法国天文学家、数学家华纳在评论帕斯卡计算机的设计思想时，曾说过，“帕斯卡的思想，特别是在当时，可以算作是非凡的勇敢。因为他提出了这样的目的，即利用纯粹机械装置，来代替我们的思考和记忆。”毫无疑问，这种非凡的思想为后人提出用机器来执行推理，以至用机器执行几何定理证明以极大的启发。

帕斯卡以后，人们又相继制造了进行加减运算，乘法运算和开方运算的机器，但是，所存在的缺陷使得它们无法适应社会发展对计算提出的要求，所以最终没有得到推广，不过他们的思想却被后人继承下来。进入21世纪后，计算机的计算速度更是大得惊人，正是这种惊人的高速度，使得计算机对数学的影响远远超出了其最初作为计算工具的功能，成为几何定理机器证明的工具。

最初是17世纪德国数理逻辑学家、哲学家和微积分的创始人之一的莱布尼兹，明确提出机器可以成为推理工具的思想，他可能是受到帕斯卡的思想和笛卡尔解析几何思想的启发，想到可以创造一种通用的语言，以实现推理的机械化，从而把很多数学问题的处理机械化。为了将几何的推理过程归结为代数的计算问题，笛卡尔创立了解析几何，帕斯卡设计的机器，可以将代数的计算问题机械化，因此，莱布尼兹想建立一种演算，可以将推理转化为计算。遗憾的是，由于所处时代的限制，莱布尼兹没有实现他的梦想，但是他的思想却被后人发展了。

定理证明历来受到人们的关注，为了完成一个定理证明，有时要花费一个人或几个人一辈子或几辈子的时间，即使如此，有时也还是找不到合适的证明。正由于定理证明的艰难，才使得在数学历史上几代人有一个共同的梦想：把定理证明特别是几何定理证明机械化。

当然，用机器实现几何定理证明无论在理论上还是在实践上都不可能是一帆风顺的。首先，用机器实现几何定理的证明甚至是推理的机械化的想法并不为所有的人接受。著名的法国数学家庞加莱就曾对这一想法大加责难，认为这种想法注定是不可能实现的。后来虽然从数理逻辑角度奠定了定理机器证明的理论基础，并得到引人注目的结论：一切初等几何和初等代数范围的命题，都可以用机械方法判定。以及1959年美籍数理逻辑学家王浩在这方面做出了鼓舞人心的工作，但是，计算机技术的发展并没有让人们顺利地在几何定理证明领域中取得成就，这又让一些人对机器定理证明产生了消极态度。(www.daowen.com)

柳暗花明又一村，1983年在美国科罗拉多州举行的全美定理机器证明学术会议上，大陆赴美求学的青年学者周咸青的报告，为自动推理领域的专家学者带来了意外的惊喜：他可以在计算机上自动地证明几百条困难的几何定理，而且一条定理证明只需几秒钟。他所运用的方法就是我国著名数学家吴文俊教授建立和发展的机器证明代数消元法——吴方法。

“吴方法”是受我国古代数学思想的影响而产生的。吴文俊教授通过对我国古代数学的研究，发现我们先人解决问题的思路可以用“机械化”一词加以概括。因为“四则运算与开平方的机械化算法由来已久。汉初完成的«九章算术»中，对开平方、开立方的机械化过程，就有详细说明，到宋代更发展到高次代数方程求数值解的机械化算法。在宋元时代，我国就创立了‘天元术’，引进了天元、地元、人元、物元等相当于现代未知数的概念，把相当多的问题特别是几何问题转化为代数方程与方程组的求解问题。这一方法用于几何可称为几何的代数化。12世纪的刘益将新法与‘古法’比较，称‘省功数倍’。与之相伴而生，又引进了相当于多项式的概念，建立了多项式的运算法则和消元法的有关代数工具，具见于宋元时代幸以保存至今的杨辉、李冶、朱世杰的许多著作中。”吴文俊教授所创立的“吴方法”正是鉴戒了我国古代数学中解方程组的思想，几何定理的机器证明可以看作是我国传统数学解方程的一个具体应用。

“欧几里得传统是公理化、演绎推理与证定理。我国传统数学则是着重解决具体问题，从问题出发，由此自然导致方程求解。”“我从事几何定理证明时，首先选取适当坐标，于是几何定理的假设与终结通常都成为多项式方程，称之为假设方程组与终结方程。满足定理假设的几何图像，就相当于假设方程的一个解答或零点。要证明定理成立，就是要证明这样的零点也使终结多项式为0。我国传统数学主要是解方程（而不是证定理），它提供了解任意多项式方程组的方法，因之提供了求得所有假设方程组的解答或零点的方法，由此解答就可检查这些零点是否也是终结方程的解答或零点，也就提供了证明几何定理的方法。”（«数学通报»2003年第6期第6页）

在几何定理的机器证明上，吴方法与以前许多方法相比较都要优越得多。