1997年吴文俊由于其在“几何自动推理领域的先驱性工作”被授予“Herbrand自动推理杰出成就奖”。该奖有国际自动推理学会颁发，用于奖励“对自动推理作出杰出贡献的个人或集体”。以前的获奖人包括自动推理创始人之一Larry Wos，自动推理创始人之一、前美国人工智能学会主席Woody Bledsoe，归结法的发明人Alan Robinson。 下面是对吴文俊先生获奖工作的介绍与评价。
“吴文俊在自动推理界以他于1977年发明的（定理证明）方法著称。这一方法是几何定理自动证明领域的一个突破。”
“几何定理自动证明首先由Herbert Gerlenter于五十年代开始研究。虽然得到了一些有意义的结果，但在“吴方法”出现之前的二十年里这一领域进展甚微。在不多的自动推理领域中，这种被动局面是由一个人完全扭转的。吴文俊很明显是这样一个人。”
“吴的工作由八十年代初期在德克萨斯大学学习的周咸青介绍给了西方学术界。周咸青（基于吴方法）的证明器证明了数百条几何定理，进一步显示了吴方法的潜力。至此，几何定理证明的研究已全面复兴，变为自动推理界最活跃与成功的领域之一。”
“吴继续深化、推广他的方法，并将这一方法用于一系列几何。包括平面几何，代数微分几何，非欧几何，仿射几何，与非线性几何。不仅限于几何，吴还将他的方法用于由Kepler定理推出Newton定理；用于解决化学平衡问题；与求解机器人方面的问题。吴的工作将几何定理证明从自动推理的一个不太成功的领域变为最成功的领域之一。在很少的领域中，我们可以讲机器证明优于人的证明。几何定理证明就是这样的一个领域。”
由于Herbrand奖是一个自动推理奖。上面的介绍侧重了吴文俊研究员在几何定理证明方面的应用。其实几何定理证明的吴方法只是吴－Ritt原理的重要应用之一。这一原理的其他应用包括：（1）求解非线性方程组的吴方法。这一方法是求解代数与微分方程组最完整的结果之一，已经被成功地用于解决很多问题。（2）吴方法还被用于若干高科技领域，得到一系列国际领先的成果。包括曲面造型,机器人机构的位置分析，智能CAD系统（计算机辅助设计）。吴文俊先生至今仍然勤奋地工作在科研第一线，不断获得具有广泛影响的科研成果。吴文俊先生91年提出良性基理论；92年提出了解方程的混合算法；93年解决了不等式证明问题；94年将吴方法用于几何设计与天体力学研究；95年提出因式分解新算法；96年后致力于微分代数几何的研究。
在国内，吴文俊先生倡导的“数学机械化”研究得到国家科委，国家自然科学基金委，中国科学院等方面的长期支持。特别是国家科委在八五、九五期间均将此项研究列入攀登项目，给予强有力的支持。这对我国继续在这一领域保持国际领先水平提供了保证。
本届“国际自动推理大会”上，美国自然科学基金委负责自动推理的A. Abdali博士主动建议由美国自然科学基金委与中国有关方面共同组织“中美几何推理及其应用”研讨会，加强两国在这一领域的合作。目前这一研讨会正在筹划中。
事实上，此前国际著名学者对吴文俊院士的工作作出过极高的评价。
1。 早在1982年，美国人工智能协会主席W. W. Bledsoe与两位McCarthy奖获得者R.S. Boyer, J.S. Moore联名致当时我国科技工作的领导人方毅，张劲夫和宋平，赞扬吴的工作是近十年中自动推理领域出现的最为激动人心的进展。信中认为：由于吴的工作，使中国的自动推理研究在国际上遥遥领先，并建议我国政府对这项研究给予充分的重视和积极支持。
2。自动推理核心刊物《自动推理杂志》全文转载吴的论文。编委J. C. Moore专门著文介绍吴的工作，认为吴的工作“不仅奠定了自动推理研究的基础，而且给出了衡量其它推理方法的明确标准”。
Distinguished Contributions to Automated Reasoning
Recipient: Professor Wu Wen-Tsun
The winner of this year's Herbrand Award,Professor Wu Wen-Tsun,is a member of the Academia Sinica,Beijing, and the founder of the Mechanized Mathematics Research Center of the Academia Sinica.
Wu is known in the automated deduction community for the method he formulated in 1977, marking a breakthrough in automated geometry theorem proving.
Geometry theorem proving was first studied in the 1950s by Herbert Gelernter and his associates. Although some interesting results were achieved, the field saw little progress for almost twenty years, until "Wu's method" was introduced. In few areas of automated deduction can one identify a specific person who turned the field around completely. Wu is clearly such a person. His work started from the observation of the (well-known) correspondence between plane geometry and analytic geometry. Specifically, one can transform a problem in elementary geometry into a set of polynomials and, by solving the polynomials, deduce the correctness of the theorem. This transformation of problems in geometry into problems in algebra enables researchers to use a full range of algebraic tools, which are much easier to automate than their counterparts in geometry. Wu based his method on Ritt's principle and a zero structure theorem for solving the polynomials. His method can be used not only to prove theorems in geometry, but also to discover theorems and to find degenerated cases automatically.
Wu started his research on geometry theorem proving in 1976, near the conclusion of the Cultural Revolution. He implemented his method on a rather primitive computer (the Great Wall 203 with 4K memory) in 1977 and proved the Simson line theorem. When visiting the United States for the first time in 1979, Wu acquired a more sophisticated computer (the HP9835A with 256K memory) and was able to prove more sophisticated problems such as the Morley theorem. S.C. Chou introduced Wu's method to the West while studying at the University of Texas in the early 1980s. Chou's prover proved several hundred theorems and further demonstrated the power of Wu's method. Geometry theorem proving was by then fully revised and became one of the most actively researched and successful areas in automated deduction.
Wu continued refining and extending his method and added a dazzling array of application domains whose proofs can be automated. They include plane geometry, algebraic differential geometry, non-Euclidean geometry, affine geometry and nonlinear geometry. Not limiting the applications to geometry alone, he also gave mechanical proofs of Newton's gravitational laws from Kepler's laws try theorem proving from one of the less successful research areas in automated deduction to one of the most successful. Indeed, there are few areas for which one can claim that machine proofs are superior to human proofs. Geometry theorem proving is such an area.
Born in Shanghai in 1919, Wu studied mathematics at the Shanghai Jiao-tung University. His education was interrupted for five years by the Sino-Japanese War. After the war. he enter the newly founded Institute of Mathematics of the Academia Sinica and resumed research in mathematics under S.S. Chern. In 1947, he went to the University of Strasbourg and studied topology under C. Ehresmann. After completing his state thesis in 1949 (on Grassmannian manifolds),he went to Paris and worked at the CNRS under E. Cartan. During his stay in France, Wu gained recognition for his work in topology. For instance, Cartan attributed the discovery of the Cartan formula to Wu. Wu also introduced what was later known as the Dold manifold.
After returning to China in 1951, Wu rejoined the Academia Sinica and continued to work in algebraic and differential topology until the Cultural Revolution. He made important contributions to the theory of Euclidean spaces and Pontrjagin theory, among other areas. he also turned the important "rational homotopy theory" created by D. Sullivan into algorithmic form, introducing a new terminology called I*-functors. Indeed, Wu's contributions to topology are no less significant than those to automated deduction.
The third area to which Wu made important contributions is the history of Chinese mathematics. His studies initiated from an ancient classic Nine Chapters of Arithmetic (dated about 100 B.C.) and its Annotations by Liu Hui (in A.D. 263). Liu also extended an ancient method for calculating the height of the sun, which apeared in the ancient script Zhoupi Suanjing (The Calculus of Zhoupi), to a general algorithm for calculating height, called Chongchashu (Double-Difference Algorithm). Liu's results were stated without explanations (or, more precisely, the explanations were lost) and were included in his work Haidau Suanjing ( the Calculus of Islands). Wu compared the various scripts and reconstructed the proofs of Liu's theorem in an ancient style, quite different from the usual Euclidean approach. He further argued that Chinese mathematics has its own tradition, which is based on computation as opposed to the axiomatic and proof approach of Western mathematics. To some extent, Wu's own work on geometry theorem proving is a demonstration of how East meets West and how the two trends of thought complement each other.