編輯：杜偉、大盤雞
本週二，我們報道了菲爾茲獎得主陶哲軒的一個開源專案 —— 在大模型的協助下編寫了一個概念驗證軟體工具，來驗證涉及任意正引數的給定估計是否成立（在常數因子範圍內）。
在專案中，他開發了一個用於自動（或半自動）證明分析中估計值的框架。估計值是 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 討論區，瞭解更多一線協作細節。
© THE END
轉載請聯絡本公眾號獲得授權
投稿或尋求報道：[email protected]
