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

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

這才幾天的時(shí)間，這個(gè)估計(jì)驗(yàn)證工具的 2.0 版本就來(lái)了！

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

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

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

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

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

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

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

具體實(shí)現(xiàn)過(guò)程

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

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

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

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

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

這里，根據(jù)使用的三種策略對(duì)證明進(jìn)行「?jìng)尉妗姑枋觯翰呗浴竎ases h」 1 對(duì)假設(shè)「 h1」進(jìn)行情況拆分，然后在兩種情況下分別應(yīng)用「simp_all」策略來(lái)簡(jiǎn)化。

該工具支持漸近估計(jì)。陶哲軒找到了一種在 Sympy 中實(shí)現(xiàn)量級(jí)形式化的方法。事實(shí)證明，Sympy 在某種意義上已經(jīng)可以原生實(shí)現(xiàn)非標(biāo)準(zhǔn)分析：它的符號(hào)變量有一個(gè)「is_number」標(biāo)志，基本上對(duì)應(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ù)量級(jí)「Theta (X)」，其屬性「 Theta (n)=Theta (1)」如下：如果「n」是標(biāo)準(zhǔn)數(shù)，然后使用這個(gè)概念來(lái)定義漸近估計(jì)，例如 （實(shí)現(xiàn)為 lesssim (X,Y)）。接下來(lái)可以應(yīng)用對(duì)數(shù)形式的線性算術(shù)來(lái)自動(dòng)驗(yàn)證一些漸近估計(jì)。這里有個(gè)簡(jiǎn)單的例子：給定一個(gè)正整數(shù) N 和正實(shí)數(shù) x,y，使得  且  ，任務(wù)目標(biāo)是得出結(jié)論 ：

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

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

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

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

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

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

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

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

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

故事就此開(kāi)始，陶哲軒選擇做一個(gè)實(shí)驗(yàn)?！肝覈L試完全基于 Bruno 的草稿，一步步進(jìn)行形式化，過(guò)程非常依賴 Copilot 和 Lean 的 canonical 策略?！顾麑⒃宀鸾獬杉?xì)小邏輯單元，讓工具處理約一半細(xì)節(jié)，剩下的由自己手動(dòng)填補(bǔ)，完成了一個(gè)可以通過(guò)驗(yàn)證的 Lean 形式化證明，還錄了視頻上傳到 YouTube。

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

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

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