陶哲軒大家都很熟了，被譽為“數學界的莫扎特”的超級大神

今天，陶神在社交媒體 Mastodon (@tao@mathstodon.xyz) 上分享了一次AI協作實驗：他嘗試使用當前流行的AI自動化工具，來形式化（formalize）一個數學證明。具體來說，他用的是GitHub Copilot配合Lean(一個依賴類型理論的證明助手) 中的canonical策略 (一個依賴類型匹配策略)

目標：搞定一個“小”證明，但需要極高精確度的“體力活”證明

這次實驗的對象，是陶哲軒在“等式理論項目 (Equational Theories Project)”中的一位合作者 Bruno Le Floch 提供的一頁紙證明。這個證明屬于泛代數領域，具體來說，是關于“原群 (magma)”（一個集合配上一個二元運算，不一定滿足結合律啥的）的一些定律

核心是要證明一個編號為 e1689 的等式

能推導出 e2 等式（x = y對任意 x, y 成立，即所謂的“單點律”）。這個推導過程充滿了繁瑣的符號操作，不涉及太多高深概念，主要考驗細節的準確性

大神“盲打”：33分鐘的AI輔助之旅

陶哲軒的目標是，以一種“低級別”、“逐行”的方式，幾乎是“盲打”地，在不深入理解證明宏觀結構的前提下，完成這個形式化過程。他想看看AI工具能在多大程度上助力這種技術性工作

你可能以為大神一出手就馬到成功？非也！陶神坦言，這是他的第三次嘗試：

• ?第一次：沒看證明，直接上手寫代碼，結果5行就卡住了，因為不理解其中一步

• ?第二次：完整地走完了流程，耗時48分鐘，但悲催的是屏幕錄制出了問題

• ?第三次（也就是這次分享的）：因為已經做過一次，所以“心中有數”，僅用33分鐘就完成了。他也幽默地提到，AI工具可能因為他之前的嘗試而被“污染”了，或許已經“記住”了部分證明。所以，這算不上一個嚴格的科學對照實驗，但足以展示過程

實驗過程亮點（濃縮版）：

1.環境搭建：首先在 Lean 中定義了“原群 (Magma)”、e1689 和 e2 等基本概念

2.逐行翻譯：陶哲軒將 Bruno 的證明拆分成一個個“原子級”的小步驟，然后逐行嘗試形式化

• ? 定義輔助對象：比如定義了函數S(x, z) = x * x * z * z和F(x, y, z) = y * S(x, z)（后來發現F其實是y * (x * (x * z * z))）。主等式 e1689 可以寫成x = F(x, y, z)

• ? Copilot 的角色：GitHub Copilot 會在他輸入時提供代碼建議。有時建議很精準，能直接采用；有時則需要手動調整，甚至會給出錯誤的中間結論，需要陶哲軒識別并修正。比如在證明 Lemma 1 的一個計算步驟中，Copilot 給出的FBC = A * B * Z就和實際需要的A * F B C（或A * Z，其中Z是SCB）不符

• ?canonical策略的運用：canonical策略在很多類型匹配上表現出色，能自動完成一些簡單的證明步驟。但陶哲軒也提到，在處理存在性量詞（比如證明“存在一個 z 使得 y = z * a”）時，canonical有時會“卡住”，需要他手動“打開”這個存在性量詞（即明確指出這個 z 是什么），canonical才能繼續工作

• ? “卡殼”與手動介入：當AI工具無法一步到位時，陶哲軒會查閱 Bruno 的原始證明，理解當前步驟的邏輯，然后使用 Lean 中更基礎的策略（如apply,exact,convert,calc計算塊等）進行手動推導，直到問題簡化到AI工具可以接手的程度

• ? Lemma 的逐個擊破：整個證明被分解為多個 Lemma (引理)

3.最終定理證明：基于前面的引理，最后證明了e1689能夠推導出e2 (a = y)。其中一個關鍵步驟是，利用 Lemma 3 得到的e，將a表示為S(e,a)，然后代入主等式進行推導

注意：以上過程只是簡單示意總結，難免出錯，數學大神請直接看陶神視頻

這是最終證明：

https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean

陶哲軒的思考：AI輔助下的新范式

實驗結束后，陶哲軒總結道：

風格迥異：這種高度依賴AI工具、逐行解決細節的方式，與他平時先理解證明“大局觀”再進行形式化的風格完全不同

效率與盲點：對于這種技術性強、概念性不那么突出、主要考驗細節準確性的證明（陶神稱之為“非概念性論證”），AI工具組合確實能有效工作。它把主要精力從“理解宏觀策略”轉移到了“確保每一步細節正確”

人機協作是關鍵：AI工具并非萬能。大約一半時間，工具能直接給出正確步驟；另一半時間，則需要人工閱讀原始證明，甚至動用“老派”的證明技巧來化簡問題，然后再讓AI接手。期間，他也因過度依賴Copilot而錯過檢查其生成的語句是否確實是證明所需要的，導致返工

“剝離概念，聚焦細節”：整個過程幾乎沒有進行高層次的策略思考，而是將證明分解為一系列“完成下一行代碼”的小問題

適用場景：這種方法可能非常適合處理那些本身就比較繁瑣、缺乏巧妙思想但又需要極高精確度的“體力活”證明

參考：

https://www.youtube.com/watch?v=cyyR7j2ChCI&t=9s

?星標AI寒武紀，好內容不錯過?

用你的贊和在看告訴我～

求贊