， 使 公理化 數學 向 構造性 數學 、 向 具有 「 現實 有效性 」 和 「 現實 可能性 」 的 機械化 數學 的 方向 轉化 ， 已 呈現出 光明 的 前景 。 自 １９９２年 以 吳文俊 為 首席 科學家 的 重大 科研 項目 「 機器 證明 及 其 應用 」 開展 以來 ， 有 中國 科學院 六 個 研究所 、 九 所 大學 和 北京市 計算 中心 的 包括 基礎 數學 、 應用 數學 、 計算 數學 、 計算機 科學 、 理論 物理 、 高 新 技術 等 研究 領域 的 學者 數十 人 （ 其中 有 中科院 院士 數 人 ） 承擔 了 該 項目 中 的 七 個 子課題 ， 包括 兩 個 基本 任務 的 子課題 （ 機證 定理 和 機解 方程 ） ， 四 個 應用 方面 的 子課題 （ 在 理論 物理 、 計算機 科學 、 數學 科學 和 機械 機構學 中 的 應用 ） 以及 軟件 系統 的 子課題 。 這些 子課題 在 五 年 間 取得 了 突出 的 成績 ， 超出 了 預計 的 目標 ， 其 主要 進展 有 ： 在 幾何 定理 可讀 證明 的 自動 生成 方面 、 在 幾何 定理 機器 證明 的 數值 方法 方面 、 在 有效 處理 多 分支 可 約升列 方面 的 工作 曾 榮獲 １９９５年 中國 科學院 自然 科學 一等 獎 ； 在 微分 幾何 定理 自動 證明 方面 、 在 發展 「 Dixon 結式 」 和 創建 「 聚篩法 」 方面 、 在 多項式 的 完全 判別 系統 及 不等式 的 機器 證明 與 機器 發現 方面 、 在 機器人 反 運動學 的 符號 算法 及 其 應用 方面 、 在 線性 系統 的 定理 證明 及 近似 定理 證明 方面 的 工作 ， 則 是 最近 兩 年 取得 的 新 成果 。 基於 特徵列法 建立 曲面 造型 設計 的 新 的 理論 和 通用 方法 ， 繼續 開展 具有 奇點 的 代數簇 的 陳省身 示性類 的 研究 ， 完成 了 二維 楊振寧 -Baxter 方程 （ 複域 上 關於 １６ 個 變量 的 ６４ 個 三 次 方程 構成 的 方程組 ） 的 求解 ， 給出 了 計算 量子群 的 機械化 算法 ， 發展 了 求解 多元 代數 系統 的 特徵值 方法 ， 建立 了 特徵值 方法 的 理論 及 可行 算法 ， 給出 了 代數簇 的 同構 判定 及 自同構群 算法 。 求出 了 六 頂角 模型 和 八 頂角 模型 中 帶 參數 的 楊振寧 -Baxter 方程 的 全部 解 ， 進一步 完善 了 離散群 的 非 交換 幾何 和 規範 理論 ， 構造性 地 給出 了 量子群 上 的 微分 運算 ， 從而 得到 了 量子群 上 的 幾何 理論 ， 以及 給出 了 量子群 的 第一 個 經典 實現 。 探討 了 吳 方法 在 計算機 視覺 、 小波 分析 、 程序 驗證 和 一階 語言 的 定理 自動 證明 中 的 應用 ， 並 拓廣 至 從 基礎 研究 的 角度 探討 思維 邏輯 的 基本 規律 以及 研究 不同 的 邏輯 系統 中 關於 自動 證明 的 一般 理論 和 方法 。 在 求解 偏微分 方程 、 研究 常微分 方程 性質 、 非線性 全 局 優化 算法 、 多元 樣條 與 CAGD （ 計算機 輔助 幾何 設計 ） 等 方面 取得 諸多 成果 。 完成 了 Stewart 平台 和 三維台 體型 的 並聯 機器人 運動學 正解 ， 以 滑動 位移 為 輸入 的 單環 空間 機構 位移 分析 及 相應 的 串聯 機械手 位移 逆解 ， 裝配 柔順 腕 機構 的 分析 ， 柔性 裝置 （ 彈簧 系統 ） 的 幾何 非線性 問題 ， 靜力 逆 分析 ， 機構 分析 與 綜合 中 經典 問題 的 現代化 處理 等 。 除了 在 項目 運作 初期 研製 的 Prover 用於 幾何 定理 的 機器 證明 以外 ， 考慮 實現 吳 方法 的 通用 的 符號 軟件 ， 在 Maple 支撐 下 完成 軟件包 CSETS 和 WSOLVE 的 開發 ， 在 Saclib 的 支撐 下 完成 SACCS 的 開發 ， 規劃 並 正在 建造 一 個 自己 的 完整 的 軟件 工具 STAR （ Small Tool for Algebraic Research ） ， 以 實現 完整 的 吳 整序 理論 。 為了 使 有別於 西方 而 具有 中國 特色 也 就 是 東方 特色 的 機械化 數學 研究 在 更 大 範圍 內 開展 ， １９９５年 ８月 吳文俊 在 北京 主持 了 第一 屆 亞洲 計算機 數學 研討會 ， 交流 數學 機械化 研究 的 經驗 。 「 繼續 發揚 中國 古代 傳統 數學 的 機械化 特色 ， 對 數學 各 個 不同 領域 探索 實現 機械化 的 途徑 ， 建立 機械化 的 數學 ， 則 是 本 世紀 以至 可能 綿亙 整 個 二十一世紀 才 能 大體 趨於 完善 的 事 。 」 但是 ， 「 我們 的 目標 是 明確 的 ， 即 是 推行 數學 的 機械化 ， 使 作為 中國 數學 傳統 的 機械化 思想 ， 光芒 普照 於 整 個 數學 的 各 個 角落 」