吳方法

機器證明是使用計算機證明定理，也稱為定理的機械證明或自動證明。作為計算機科學的一個重要課題，它的研究與發展至今約有50年的歷史。

機器證明研究領域的範圍要廣泛得多。在國外則更一般地叫做自動推理。我們把幾何定理機器證明和非線性代數方程組作為主攻方向，一方面是因為吳文俊先生在70年代的突出工作，使中國在此方向上具有了領先的優勢；另一方面，這兩個方向有鮮明的應用背景，近年來在機器證明領域也確是十分活躍的，值得重視。由於傳統的興趣和多種原因，幾何定理的機器證明在自動推理的研究中佔有重要的地位。

1940年畢業於上海交通大學數學系。1979年至現在任中國科學院系統科學研究所副所長、名譽所長、研究員。

吳文俊院士是著名的數學家，他的研究工作涉及到數學的諸多領域。在多年的研究中取得了豐碩成果。其主要成就表現在拓撲學和數學機械化兩個領域。他為拓撲學做了奠基性的工作。他的示性類和示嵌類研究被國際數學界稱為“吳公式”，“吳示性類”，“吳示嵌類”，至今仍被國際同行廣泛引用，影響深遠，享譽世界。

用計算機自動證明某一類型幾何定理，甚至某一種幾何全部定理的原理和方法。從理論角度看，幾何定理的機器證明要經歷公理化、代數化與坐標化、機械化等步驟，才能編製程序並在計算機上實現。可用機器證明的幾何定理（主要是初等幾何的定理）有三種不同類型，與之對應則有三種不同的機器證明方法。每一類型定理的機器證明都必須假設代數化與坐標化已經完成，而且可把幾何定理的證明問題化為一些代數關係式的處理問題。①第一類型定理的特徵是假設部分的所有代數關係式對於某些特定變數都必須是線性的，包括一類構造型的純交點定理，其對應的機器證明方法稱為希爾伯特方法；②第二類型定理的特徵是假設和終結部分的代數關係式都可用多項式的方程來表示，其對應的機器證明方法是中國數學家吳文俊首先提出的，稱為吳文俊方法；③第三類型定理的特徵是假設和終結部分可以是任意的多項式等式或不等式，但其係數必須在一實閉域中，因而原來的幾何必須有次序關係，其對應的機器證明方法稱為塔斯基方法。這三種方法各有其適用範圍，但就可以通用的那些定理證明問題來說，希爾伯特法效率最高而塔斯基法效率最低，但是前者的適用範圍很窄。1980年在 機上，用吳文俊方法成功地證明了勾股定理、西姆遜線定理、帕普斯定理、帕斯卡定理、費爾巴哈定理，並在45個帕斯卡點中發現了20條帕斯卡圓錐曲線，這種方法還推廣到微分幾何，將微分幾何曲線論中的貝屈朗定理推廣到仿射微分幾何。吳文俊的研究成果引起了國際學術界的重視。