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

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

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

陶哲軒對該工具進(jìn)行了兩次全面改進(jìn)。

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

陶哲軒認(rèn)為現(xiàn)在得到了一個穩(wěn)定的框架，并可以進(jìn)一步擴(kuò)展該工具。他最初的目標(biāo)只是自動化（或半自動化）標(biāo)量函數(shù)漸近估計的證明，但原則上可以繼續(xù)向該工具添加策略、新的 sympy 類型和引理，以處理范圍廣泛的其他數(shù)學(xué)任務(wù)。 

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

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

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

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

具體實現(xiàn)過程

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

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

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

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

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

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

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

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

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

對數(shù)線性規(guī)劃求解器還可以通過相當(dāng)強(qiáng)力的「分支」方法處理低階項。

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

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

數(shù)學(xué)形式化證明實驗紀(jì)實

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

他最近嘗試了一個小實驗：嘗試?yán)矛F(xiàn)代自動化工具（如 GitHub Copilot 和 Lean 證明助手）來半自動地形式化一個一頁紙的數(shù)學(xué)證明。這個證明來自他在 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

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

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

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

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

實際證明， 雖然這種方法看起來有點機(jī)械，但對于結(jié)構(gòu)不強(qiáng)、以技術(shù)推導(dǎo)為主的證明，是有效的。AI 工具可以代勞大量繁瑣推理，讓人專注于「如何表達(dá)」而不是「是否合理」。

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

如果你對這個話題感興趣，建議直接查看 Zulip 討論區(qū)，了解更多一線協(xié)作細(xì)節(jié)。