一般地，幾何定理機器證明問題可以分成下面兩個主要步驟：
第一步，用解析幾何方法建立座標系設未知量，將條件表示成所設未知量的多項式方程組G1，將求證表示成多項式方程組G2.（幾何的代數化與座標化）
我們也分這兩步來介紹。第一步只要看一個簡單的例子：射影定理的代數化
求證：直角三角形斜邊上的高是斜邊兩線段的比例中項。
建立座標系、設未知量如：
l 條件代數化：
1. AD垂直於BC，斜率互為負倒數，整理得：h1(u1, u2, x1, x2) = x1u1–x2u2 = 0
2. D在BC所在直線上，整理得：h2(u1, u2, x1, x2) = x1u2–x2u1–u1u2 = 0
條件是四元二次多項式方程組
l 求證代數化：
|AD|2 = |CD|·|BD|, 整理得：
g1(u1, u2, x1, x2) =
結論G2: g1(u1, u2, x1, x2) = 0
第二步也就是機械化的核心步驟：判斷G2是否可以由G1推出。這樣的問題就我們目前所學實在無能為力，甚至說清“推出”二字也很難。比較明顯地我們說可以推出x2–y2–4 = 0還可以推出x = 0等，但是對多元高次的多項式方程組我們就必須藉助高等的數學工具和計算機演算法來幫忙了。
一種可行的演算法是藉助前面提過的Grobner基的性質，用計算機去求由多項式組{hi}和g生成的一種代數結構的Grobner基（一組多項式），看這組基中是否包含數字1來判斷是否可以推出結論g = 0.
吳方法同樣是由{hi}構造一組多項式，稱為廣義特徵列。判斷g = 0對廣義特徵列的擬除餘式是否為0，就知道求證是否成立了。
上述演算法很難理解，事實上多項式方程組求解的問題非常困難，對這個問題的探索理論上引發了代數幾何學的建立。我們試著用簡單的語言對上面的方法作一點解說：（解釋原理，數學上不一定精確）
要證多項式方程g = 0由多項式方程組{hi = 0}推出，就是要證：
g = c1h1 + c2h2 +…+ cnhn, 其中{ci}是和g, {hi}含有相同變元的多項式組。一種樸素的想法是g關於{hi}做除法：用h1去除g, 再用h2去除餘式m1, 再用h3去除餘式m2……只要最後hn除餘式mn-1為0即可。但是由射影定理的例子可見g關於{hi}實行這樣的除法是行不通的。於是我們想辦法轉化：Grobner基與廣義特徵列都是多項式組{pi}，使得所有寫成d1p1 + d2p2 +…+ dmpm形式的多項式的0點集合就是所有c1h1 + c2h2 +…+ cnhn形式多項式的0點集合（這個集合是令多項式為0的各變元取值的集合，幾何上稱仿射簇，可以理解為保證多項式方程組同解）。於是問題轉化成證明g = d1p1 + d2p2 +…+ dmpm，由於Grobner基與廣義特徵列具有很好的代數性質，兩種演算法都可以採用類似多項式除法的辦法進行驗證。Gröbner基方法中考慮g模{pi}約化的正規化（類似於前述多項式除法的最終餘式），正規化為0說明g = 0 可由{pi = 0}推出，定理得證。吳方法中考慮g關於{pi}擬除的餘式Rem(g, {pi}), 餘式為0定理得證。
需要指出的是求Grobner基與廣義特徵列的過程同時也是多項式方程組消元的過程，比證明g = 0用途更廣泛的是這兩種方法同時給出了求解多項式方程組的有效演算法（即使不能求出每個未知量，至少可以保證同解地消掉其中的一部分變元，因而也可用於多引數方程組消參），宏觀上這類似前面正文討論的消元法，因此吳方法也被稱為吳消元法。同時吳文俊先生大力倡導數學機械化的應用，如應用於線性控制系統、機構綜合設計、平面星體執行的中心構形、化學反應方程的平衡、代數曲面的光滑拼接、從開普勒定律自動惟出牛頓定律、全域性最佳化求解等等。在他的指導和帶動下，數學機械化方法還在一些交叉研究領域獲得初步應用，如理論物理、計算機科學、資訊科學、自動推理、工程幾何、機械機構學等等。數學機械化研究正不斷開拓更多的應用領域。
關於幾何定理的機器證明最後再談兩點，其一文中介紹的Grobner基方法由於在求基的過程中引入大量中間多項式，又可能出現複雜的有理係數，該演算法會佔用大量的處理時間和儲存空間在定理證明中效率遠不如吳方法高。二者效率詳細對比和大量機證實驗可參見http://zhwzh.bj4hs.edu.cn/paper/main.html. 最後一點引用吳文俊先生的話總結數學機械化的實質：
“把質的困難轉化為量的複雜。”
這不也是演算法思想的實質嗎？
一般地，幾何定理機器證明問題可以分成下面兩個主要步驟：
第一步，用解析幾何方法建立座標系設未知量，將條件表示成所設未知量的多項式方程組G1，將求證表示成多項式方程組G2.（幾何的代數化與座標化）
我們也分這兩步來介紹。第一步只要看一個簡單的例子：射影定理的代數化
求證：直角三角形斜邊上的高是斜邊兩線段的比例中項。
建立座標系、設未知量如：
l 條件代數化：
1. AD垂直於BC，斜率互為負倒數，整理得：h1(u1, u2, x1, x2) = x1u1–x2u2 = 0
2. D在BC所在直線上，整理得：h2(u1, u2, x1, x2) = x1u2–x2u1–u1u2 = 0
條件是四元二次多項式方程組
l 求證代數化：
|AD|2 = |CD|·|BD|, 整理得：
g1(u1, u2, x1, x2) =
結論G2: g1(u1, u2, x1, x2) = 0
第二步也就是機械化的核心步驟：判斷G2是否可以由G1推出。這樣的問題就我們目前所學實在無能為力，甚至說清“推出”二字也很難。比較明顯地我們說可以推出x2–y2–4 = 0還可以推出x = 0等，但是對多元高次的多項式方程組我們就必須藉助高等的數學工具和計算機演算法來幫忙了。
一種可行的演算法是藉助前面提過的Grobner基的性質，用計算機去求由多項式組{hi}和g生成的一種代數結構的Grobner基（一組多項式），看這組基中是否包含數字1來判斷是否可以推出結論g = 0.
吳方法同樣是由{hi}構造一組多項式，稱為廣義特徵列。判斷g = 0對廣義特徵列的擬除餘式是否為0，就知道求證是否成立了。
上述演算法很難理解，事實上多項式方程組求解的問題非常困難，對這個問題的探索理論上引發了代數幾何學的建立。我們試著用簡單的語言對上面的方法作一點解說：（解釋原理，數學上不一定精確）
要證多項式方程g = 0由多項式方程組{hi = 0}推出，就是要證：
g = c1h1 + c2h2 +…+ cnhn, 其中{ci}是和g, {hi}含有相同變元的多項式組。一種樸素的想法是g關於{hi}做除法：用h1去除g, 再用h2去除餘式m1, 再用h3去除餘式m2……只要最後hn除餘式mn-1為0即可。但是由射影定理的例子可見g關於{hi}實行這樣的除法是行不通的。於是我們想辦法轉化：Grobner基與廣義特徵列都是多項式組{pi}，使得所有寫成d1p1 + d2p2 +…+ dmpm形式的多項式的0點集合就是所有c1h1 + c2h2 +…+ cnhn形式多項式的0點集合（這個集合是令多項式為0的各變元取值的集合，幾何上稱仿射簇，可以理解為保證多項式方程組同解）。於是問題轉化成證明g = d1p1 + d2p2 +…+ dmpm，由於Grobner基與廣義特徵列具有很好的代數性質，兩種演算法都可以採用類似多項式除法的辦法進行驗證。Gröbner基方法中考慮g模{pi}約化的正規化（類似於前述多項式除法的最終餘式），正規化為0說明g = 0 可由{pi = 0}推出，定理得證。吳方法中考慮g關於{pi}擬除的餘式Rem(g, {pi}), 餘式為0定理得證。
需要指出的是求Grobner基與廣義特徵列的過程同時也是多項式方程組消元的過程，比證明g = 0用途更廣泛的是這兩種方法同時給出了求解多項式方程組的有效演算法（即使不能求出每個未知量，至少可以保證同解地消掉其中的一部分變元，因而也可用於多引數方程組消參），宏觀上這類似前面正文討論的消元法，因此吳方法也被稱為吳消元法。同時吳文俊先生大力倡導數學機械化的應用，如應用於線性控制系統、機構綜合設計、平面星體執行的中心構形、化學反應方程的平衡、代數曲面的光滑拼接、從開普勒定律自動惟出牛頓定律、全域性最佳化求解等等。在他的指導和帶動下，數學機械化方法還在一些交叉研究領域獲得初步應用，如理論物理、計算機科學、資訊科學、自動推理、工程幾何、機械機構學等等。數學機械化研究正不斷開拓更多的應用領域。
關於幾何定理的機器證明最後再談兩點，其一文中介紹的Grobner基方法由於在求基的過程中引入大量中間多項式，又可能出現複雜的有理係數，該演算法會佔用大量的處理時間和儲存空間在定理證明中效率遠不如吳方法高。二者效率詳細對比和大量機證實驗可參見http://zhwzh.bj4hs.edu.cn/paper/main.html. 最後一點引用吳文俊先生的話總結數學機械化的實質：
“把質的困難轉化為量的複雜。”
這不也是演算法思想的實質嗎？