數學機械化

數學機械化是我國數學家開創的基礎研究領域。20多年來，吳文俊先生身體力行、滿腔熱情地倡導數學機械化研究，其內容、方法和意義日益獲得科學界的理解和贊同。

（計算機證明數學問題）是由吳文俊提出，華人美籍數學家王浩也是最初的研究人員之一，它是極為神奇的超級工程數學，有可能引發工程技術的革命和某些基礎數學的革命。

是研究數量關係和形體性質的科學。“數”與“形”在現實世界中無處不在，因此，數學科學是自然科學的基礎，也是高新技術的基礎，甚至是工程建設的基礎，這已是人們的共識。數學科學的好處是，可以化難為易，把奧妙變為常識，為各類問題的解決提供框架。

在產業革命的進程中，各類機器不斷問世，逐步實現著體力勞動的機械化。這已延續了數百年。伴隨著這一過程，自然科學獲得了巨大進步，數學科學取得了現代數學的偉大發現。如今，人類社會正步入信息革命時代。計算機的功能不斷增強，人類社會開始逐步實現腦力勞動的機械化。數學研究是典型的腦力勞動，具有論證嚴謹、表述明確等優點，理應率先實現機械化。

20世紀70年代，吳文俊先生研讀中國數學史。中國古代數學，既有系統的理論，又有豐碩的成果，這些成果經常以演演算法（術）的方式表述，其理論依據則總結為一些原理。直到16世紀，中國數學在很多分支都在國際上遙遙領先，是名副其實的數學強國。吳文俊先生提出，數學機械化思想貫穿於中國傳統數學，數學機械化思想是我國古代數學的精髓。他分析了中國傳統數學的光輝成就在數學科學進步歷程中的地位和作用，明確指出，源於西方的公理化思想和源於中國的機械化思想，對於數學的發展都發揮了巨大作用，理應兼收並蓄。如今，計算機科學被認為是演演算法的科學。以演演算法為核心的機械化思想，既傳統又前瞻，將為信息時代數學科學的創新發揮重大作用。

數學機械化研究，是在初等幾何定理的機器證明研究方面取得突破的。公理化體系的幾何定理證明非常不機械化。以中學課程中的幾何為例，－個定理的證明，往往要經過冥思苦想，奇巧構思，無章可循地填加輔助線，迂迴曲拆地給出證明。如何利用計算機進行自動推理，特別是進行幾何定理的自動證明，是學術界長期研究的課題。所謂定理的機械化證明，就是對一類定理（這類定理可能成千上萬）提供一種統一的方法，使得該類定理中每個定理，都可依此方法給出證明。在證明過程中，每前進一步，都有章可循地確定下一步該做什麼和如何做。從“一理一證”到“－類一證”，是數學的認識和實踐的飛躍。吳先生創立了初等幾何（泛指不具有微分運算的幾何，如歐氏幾何、非歐幾何、仿射幾何、投影幾何、代數幾何等等）定理證明的機械化方法，國際上稱“吳方法”，首次實現了高效的幾何定理的機器證明。“吳方法”也可用於幾何定理的自動發現和未知關係的自動推導。吳文俊先生的開創性成果，打破了國際自動推理界在幾何定理自動證明研究中長期徘徊不前的局面，也使我國在這一領域處於領先地位。吳先生的傑出貢獻，使他獲得1998年度國際自動推理界的最高獎“Herbrand獎”。（此獎每兩年頒發一次，每屆最多授予一人，迄今為止，獲獎者均為自動推理界的領袖人物。）

幾何學包括定理證明、幾何作圖和幾何不等式證明。在吳先生開創性成果的影響和啟迪下，在幾何學的機械化方面，如定理機器證明、幾何自動作圖和幾何不等式機器證明，我國學者都取得了很大成績。這個領域也開始吸引外國學者向我們學習。

眾所周知，直線和平面等幾何概念可由一次代數方程描述，多項式方程則用於描述曲線和曲面等。數學科學中，從線性到非線性的第一步跨躍，是由多項式實觀的。因此，多項式方程組求解是非線性數學最基本的課題，這個問題的研究已經持續幾百年。數學不同分支中許多的問題、自然科學不同領域中很多的問題、高新技術中大量的問題，都可轉化為多項式方程組求解。在幾何定理機器證明的過程中，必須理清多項式方程組的零點結構。這一需求，促使吳先生創立了多項式方程組求解的理論和方法，國際上稱“特徵列法”或“吳消元法”。吳先生還把這些方法拓展到微分情形，建立了微分幾何定理機器證明和微分代數方程組求解的機械化理論和方法。自然，較之代數情形，微分代數的應用範圍更為廣闊，同時，問題的研究更為複雜和困難。

證定理和解方程，大體上涵蓋了數學活動的主要內容。在機證定理和機解方程兩個方面，吳文俊先生在理論和方法上都做出了原創性的貢獻。

吳文俊先生強調：“數學機械化方法的應用，是數學機械化研究的生命線”。他本人的研究工作己涉及許多應用領域，如線性控制系統、機構綜合設計、平面星體運行的中心構形、化學反應方程的平衡、代數曲面的光滑拼接、從開普勒定律自動惟出牛頓定律、全局優化求解等等。在他的指導和帶動下，數學機械化方法己在一些交叉研究領域獲得初步應用，如理論物理、計算機科學、信息科學、自動推理、工程幾何、機械機構學等等。數學機械化研究不斷開拓更多的應用方面。

吳文俊先生說過，從事數學研究，要有良好的思維方式，在思想觀念上要有所突破。許多事例表明，－些數學分支正是由於踏上了機械化的道路而獲得了蓬勃的發展，使之成為重要的研究方向，甚至成為數學的主流。這是因為，抽象的數學概念和結論，往往是難於掌握和運用的。當把抽象的概念變成具體可算的（演演算法經常用公式表達），既有定性的結論又有定量的計算，數學理論才臻於完善，易於接受和適宜應用。運用機械化思想考察數學，將會發現數學的不同側面，建立新的模式，活躍和啟迪數學家的思維，從而產生大量的原始創新。

在信息革命時代，數學將出現什麼樣的變化？尤其是，中國的數學將如何進步？這是數學家們經常思考的問題。倡導和開展數學機械化研究，則為中國數學的發展提出了一種戰略導向。如今數學機械化研究剛剛處於起步階段。吳文俊先生制定的目標十分明確：讓數學機械化思想普照數學的各個角落。這是將要綿延幾代人的事業，需要各個方面專家的參與和共同努力。