編者按：本文首次發表作者珍藏的王浩1978年4月10號寫給吳文俊的信。
吳文俊先生幾天前（2017年5月7日）過世了， 差幾天就到他九十八歲生日。 5月13日又是王浩逝世二十二年的紀念。 吳先生長王先生兩歲， 兩人都是五月來五月去。
天才Wolfram有個習慣， 每逢他敬仰的人的生日或辭世日， 他都會在他博客上發文追思。 王浩和吳文俊， 他們的學問遠超過我的智力所及， 本沒有資格懷念。 今天寫幾段話講講王浩和吳文俊的交往。
吳文俊先生對中國傳統數學的捍衛
吳文俊先生是數學家中的人精。 “文革”前他就在關肇直影響下，
同年， 他的文章“初等幾何判定問題與機器證明”發表在《中國科學》上。 吳文俊聲稱他的成果是在研究中國數學史時， 受到啟發。 老一代人對中國傳統的捍衛無法以理性解釋。
1978年， 吳文俊先生全家福 （左起：吳月明、吳文俊、吳雲奇、吳天驕、吳星稀、陳丕和）
哥德爾證明一階整數（算術）是不可判定的， 但塔爾斯基則證明一階實數（初等幾何和代數）是可判定的。 塔爾斯基一直自認為他應該是和哥德爾比肩的邏輯學家。 塔爾斯基的結果意味著可以存在演算法能對所有初等幾何和代數問題給出證明。
塔爾斯基的原始演算法是超指數的， 在被後人多次改進之後仍然很難被當作通用演算法。
王浩與吳文俊的通信：兩種定理證明之間為數不多的交流
周鹹青（Chou Shang-ching）1978年在中科院研究生院旁聽了吳文俊的幾何定理證明的課， 那時吳文俊的《幾何定理機器證明的基本原理》還沒正式出版， 但周鹹青已拿到書稿。 他後來到德克薩斯大學奧斯丁分校留學， 師從波爾（Boyer）和布萊索（Bledsoe）， 這兩位元雖都是邏輯系定理證明的大咖， 但他們足夠寬容， 讓周鹹青對自己的博士論文題目自作主張， 周的論文基本就是吳方法的實現。 奧斯丁分校的硬體設備當然比吳文俊的環境好多了， 周取得的成果自然也更加豐富。
王浩在得知吳文俊的結果後，
基於邏輯的定理證明器最適合解決代數問題，
1979年吳文俊的工作得到楊振寧的關注， 當時的科學院副院長李昌和剛成立的科學院系統所所長關肇直都大力支持吳文俊， 並為他申請到兩萬美元去美國購買一台家用電腦， 以實現他的吳方法。 吳文俊到美國的重要一站是去洛克菲勒大學會見王浩。 吳文俊的工作在定理證明界迅速引起重視， 王浩起了關鍵的推動作用。 吳文俊1997年獲得第四屆Herbrand獎， 這是定理證明領域的最高獎項。在他前面獲獎的有沃思（Wos）、布萊索和發明歸結演算法的羅賓遜（Robinson），馬丁·大衛斯遲至2005年才獲獎。
吳文俊的長壽也體現在他的學術生命。1979年吳文俊六十高齡開始學習電腦程式設計語言，先是BASIC，後又Algol，再後又Fortran。他在那台兩萬美元的家用電腦上不斷取得新的成果。後來系統所的硬體設施改進，吳文俊在相當一段時間裡都是上機時間最長的。
每一次數學的突破，都以腦力勞動的機械化體現
物理學怪才兼企業家弗裡德金（Edward Fredkin）曾為電腦下棋設立過獎項。但不大為人所知的是他為機器定理證明也設立過一個獎項，分三等，第三等是當前成果獎（Current），1983年沃思和溫克獲獎，1991年波爾和摩爾獲獎。二等獎是里程碑獎，1983年給了王浩，1984年給了羅賓遜，1991年給了布萊索。一等獎被稱為萊布尼茨獎（注意：和德國的那個萊布尼茨獎不同），一次也沒發出過，因為條件是“不僅夠格在數學雜誌上發表，還要夠格評選美國數學會的Cole獎或Veblen獎，甚至菲爾茨獎”。
弗裡德金為電腦下棋設定的幾個獎項有明確的標準：戰勝特級大師，戰勝當前世界冠軍。按此標準就不難理解為什麼馬庫恩（McCune）的羅賓斯猜想的機器證明尚不夠格一等獎。馬庫恩的前老闆、定理證明的領袖人物沃思（Larry Wos）認為馬庫恩應該很接近了。但該獎的評委、哈佛數學家大衛·芒福德（David Mumford）想都不想地說：“現在不行，一百年都夠嗆（Not now, not 100 years from now）。”
隨著定理證明事業的凋零，該獎後來也悄無聲息地撤銷了。也有樂觀派：離散數學家格雷漢姆（Ron Graham ，他的太太是另一位成果豐富的離散數學家Fan Chung金芳蓉）認為在證明定理上電腦超過人是遲早的事，人腦畢竟是生物進化的產物，天生的目的不是用來證明定理的。
吳文俊的哲學思想是典型的數學家思路，這和邏輯學家不盡相同。吳老一次講座中講電腦和數學機械化，引用維納的說法：“人腦貶值，至少人腦所起的較簡單、較具常規性質的判斷作用，將貶值。”笛卡兒認為代數使得數學機械化，因而使得思考和計算步驟變得容易，無需花很大腦力。小學算術很難的東西，初中代數立個方程馬上就解了。每一次數學的突破，往往以腦力勞動的機械化體現。我想吳老應該算樂觀派。
楊振寧曾說他自己最重要的成就是提高了中國人的自信。陳省身、華羅庚、楊振寧、李政道那一批人是最早為人類文明做出點貢獻的中國人。我想那個不長的名單裡還應該有王浩和吳文俊。
附
王浩1978年寫給吳文俊的信
吳文俊的長壽也體現在他的學術生命。1979年吳文俊六十高齡開始學習電腦程式設計語言，先是BASIC，後又Algol，再後又Fortran。他在那台兩萬美元的家用電腦上不斷取得新的成果。後來系統所的硬體設施改進，吳文俊在相當一段時間裡都是上機時間最長的。
每一次數學的突破，都以腦力勞動的機械化體現
物理學怪才兼企業家弗裡德金（Edward Fredkin）曾為電腦下棋設立過獎項。但不大為人所知的是他為機器定理證明也設立過一個獎項，分三等，第三等是當前成果獎（Current），1983年沃思和溫克獲獎，1991年波爾和摩爾獲獎。二等獎是里程碑獎，1983年給了王浩，1984年給了羅賓遜，1991年給了布萊索。一等獎被稱為萊布尼茨獎（注意：和德國的那個萊布尼茨獎不同），一次也沒發出過，因為條件是“不僅夠格在數學雜誌上發表，還要夠格評選美國數學會的Cole獎或Veblen獎，甚至菲爾茨獎”。
弗裡德金為電腦下棋設定的幾個獎項有明確的標準：戰勝特級大師，戰勝當前世界冠軍。按此標準就不難理解為什麼馬庫恩（McCune）的羅賓斯猜想的機器證明尚不夠格一等獎。馬庫恩的前老闆、定理證明的領袖人物沃思（Larry Wos）認為馬庫恩應該很接近了。但該獎的評委、哈佛數學家大衛·芒福德（David Mumford）想都不想地說：“現在不行，一百年都夠嗆（Not now, not 100 years from now）。”
隨著定理證明事業的凋零，該獎後來也悄無聲息地撤銷了。也有樂觀派：離散數學家格雷漢姆（Ron Graham ，他的太太是另一位成果豐富的離散數學家Fan Chung金芳蓉）認為在證明定理上電腦超過人是遲早的事，人腦畢竟是生物進化的產物，天生的目的不是用來證明定理的。
吳文俊的哲學思想是典型的數學家思路，這和邏輯學家不盡相同。吳老一次講座中講電腦和數學機械化，引用維納的說法：“人腦貶值，至少人腦所起的較簡單、較具常規性質的判斷作用，將貶值。”笛卡兒認為代數使得數學機械化，因而使得思考和計算步驟變得容易，無需花很大腦力。小學算術很難的東西，初中代數立個方程馬上就解了。每一次數學的突破，往往以腦力勞動的機械化體現。我想吳老應該算樂觀派。
楊振寧曾說他自己最重要的成就是提高了中國人的自信。陳省身、華羅庚、楊振寧、李政道那一批人是最早為人類文明做出點貢獻的中國人。我想那個不長的名單裡還應該有王浩和吳文俊。
附
王浩1978年寫給吳文俊的信