本周二，我們報道了菲爾茲獎得主陶哲軒的一個開源項目 —— 在大模型的協助下編寫了一個概念驗證軟件工具，來驗證涉及任意正參數的給定估計是否成立（在常數因子范圍內）。

在項目中，他開發了一個用于自動（或半自動）證明分析中估計值的框架。估計值是 X?Y（在漸近記法中表示 X=O (Y)）或 X?Y（在漸近符號中表示 X=o (Y)）形式的不等式。

這才幾天的時間，這個估計驗證工具的 2.0 版本就來了！

陶哲軒對該工具進行了兩次全面改進。

首先，他將其改造成一個基礎的證明助手（proof assistant），同時能夠處理一些命題邏輯；接著，他根據評論者的反饋，將其改造成一個更加靈活的證明助手（在幾個關鍵方面特意模仿了 Lean 證明助手），它也由功能強大的 Python 符號代數包 sympy 提供支持。

陶哲軒認為現在得到了一個穩定的框架，并可以進一步擴展該工具。他最初的目標只是自動化（或半自動化）標量函數漸近估計的證明，但原則上可以繼續向該工具添加策略、新的 sympy 類型和引理，以處理范圍廣泛的其他數學任務。 

該證明助手的 2.0 版本已經上傳到了 GitHub。同樣地，與自己以前的編碼一樣，陶哲軒最終「嚴重」依賴大語言模型的幫助來理解 Python 和 sympy 的一些細節，其中 Github Copilot 的自動補全功能尤其有用。

雖然該工具支持全自動證明，但陶哲軒決定現在更多地關注半自動交互式證明，其中人類用戶提供高級「策略」，然后證明助手執行必要的計算，直到證明完成。

GitHub 地址：https://github.com/teorth/estimates

根據項目簡介，這是一個利用 Python 開發的輕量級證明助手，其功能遠遜于 Lean、Isabelle 或 Rocq 等完整證明助手，但希望它能夠輕松用于證明一些簡短而繁瑣的任務，例如驗證一個不等式或估計是否由其他不等式或估計推導出來。該助手的一個具體目標是為漸近估計（asymptotic estimates）提供支持。

具體實現過程

下載相關文件后，即可在 Python 中啟動證明助手，只需輸入「from main import *」并加載一個預先制作的練習即可。以下是其中一個練習：

這是證明助手對以下問題的形式化描述：如果 x, y, z 是正實數，且 x<2y 且 y<3z+1，則證明 x<7z+2。

證明助手的工作方式是：用戶指示助手使用各種「策略」來簡化問題，直到問題得到解決。在本例中，該問題可以通過線性算法求解，具體形式化為「Linarith ()」策略：

如果有人想更詳細地了解線性算法的工作原理，可以使用「verbose」標志（flag）來運行此策略。

有時，證明過程會涉及情況拆分，最終的證明會呈現出樹狀結構。這里有個例子：其務是證明假設 (x>-1)∧(x<1) 且 (y>-2)∧(y<2) 蘊涵 (x+y>-3)∧(x+y<3)：

這里，根據使用的三種策略對證明進行「偽精益」描述：策略「cases h」 1 對假設「 h1」進行情況拆分，然后在兩種情況下分別應用「simp_all」策略來簡化。

該工具支持漸近估計。陶哲軒找到了一種在 Sympy 中實現量級形式化的方法。事實證明，Sympy 在某種意義上已經可以原生實現非標準分析：它的符號變量有一個「is_number」標志，基本上對應于非標準分析中「標準」數的概念。

舉例而言，數字 3 的「sympy」版本「S (3)」有「S (3).is_number == True」，因此是標準的；而整數變量「n = Symbol ("n", integer=true)」有「n.is_number == False 」，因此是非標準的。

在「sympy」中，他能夠構建各種（正）表達式「X」的數量級「Theta (X)」，其屬性「 Theta (n)=Theta (1)」如下：如果「n」是標準數，然后使用這個概念來定義漸近估計，例如 （實現為 lesssim (X,Y)）。接下來可以應用對數形式的線性算術來自動驗證一些漸近估計。這里有個簡單的例子：給定一個正整數 N 和正實數 x,y，使得  且  ，任務目標是得出結論 ：

對數線性規劃求解器還可以通過相當強力的「分支」方法處理低階項。

陶哲軒計劃開始開發用于估計符號函數的函數空間范數工具，例如創建一些策略來部署諸如 Holder 不等式和 Sobolev 嵌入不等式之類的引理。Sympy 框架看起來足夠靈活，可以為這些類型的對象創建更多對象類。目前，他只有一個概念驗證引理來說明這個框架，即算術平均 - 幾何平均（arithmetic mean-geometric mean）引理。 

陶哲軒最后表示，他對這個證明助手的基本框架非常滿意，因此愿意接受進一步的建議或新功能的貢獻，例如引入新的數據類型、引理和策略，或者一些示例問題。這些問題應該很容易被這個助手解決，但目前由于缺乏合適的策略和引理而超出了它的能力。

數學形式化證明實驗紀實

而就在剛剛，陶哲軒又發了一個新項目。

他最近嘗試了一個小實驗：嘗試利用現代自動化工具（如 GitHub Copilot 和 Lean 證明助手）來半自動地形式化一個一頁紙的數學證明。這個證明來自他在 Equational Theories Project 中的合作者 Bruno Le Floch。  

• 視頻演示：https://www.youtube.com/watch?v=cyyR7j2ChCI
• 討論地址：https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Alternative.20proofs.20of.20E1689.E2.8A.A2E2
• GitHub 鏈接：https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean

陶哲軒嘗試「盲做」這個證明，即不真正理解證明結構的前提下，直接用工具去拼出形式化過程。他用約 33 分鐘完成了形式化過程。對他來說，這是一種很不一樣的工作方式 —— 不靠對整個證明的大局理解，而是完全依賴于工具處理邏輯細節。

在 Zulip 討論中，Bruno Le Floch 最初指出，在論文中「E1689-E2 的所有已知證明都是計算機輔助」這一說法太絕對了。他自己后來給出了一個更具可讀性的「人類版本」，雖有些步驟靈感來自 prover9，但整體不應算作純計算機證明。

陶哲軒回應：那我們可以更新 blueprint，并在論文中注明我們在項目中得到了一個非計算機生成的版本。

故事就此開始，陶哲軒選擇做一個實驗。「我嘗試完全基于 Bruno 的草稿，一步步進行形式化，過程非常依賴 Copilot 和 Lean 的 canonical 策略。」他將原稿拆解成細小邏輯單元，讓工具處理約一半細節，剩下的由自己手動填補，完成了一個可以通過驗證的 Lean 形式化證明，還錄了視頻上傳到 YouTube。

實際證明， 雖然這種方法看起來有點機械，但對于結構不強、以技術推導為主的證明，是有效的。AI 工具可以代勞大量繁瑣推理，讓人專注于「如何表達」而不是「是否合理」。

這場實驗還暴露出一些 Lean 項目協作工具的問題。目前項目使用的 blueprint 工具只支持每個命題綁定一個證明版本。如果要同時記錄人類證明和 AI 生成的版本，會發生覆蓋，管理混亂。

如果你對這個話題感興趣，建議直接查看 Zulip 討論區，了解更多一線協作細節。