vltanh/將數學論文形式化為Lean 4

將數學論文形式化為Lean 4 是做什麼的？

你交付一個Lean專案，以及關於它的文件，在該專案中：

• 論文證明的每個結果都使用論文自身的論證來證明。唯有在必要時，證明才能偏離論文，且每次偏離都必須報告（規則，「忠實的證明」）；
• 論文在證明中引用的每個結果也都得到證明：在Mathlib、其他公開函式庫中，或在External/中。被引用的結果可能需要某個Lean函式庫尚未具備、且該專案無法合理建構的數學內容。這樣的結果將成為使用它的每個陳述的具名假設，然後形式化將直白地表示它是條件性的；
• 陳述的內容與論文一致，每次偏離都必須記錄；
• lake build成功，且沒有sorry（Challenge.lean中的陳述除外，這是設計上的）、沒有admit、也沒有專案層級的axiom。函式庫中的每個宣告僅依賴於propext、Classical.choice和Quot.sound；
• REPORT.md審計論文與形式化的對應。它會以接下來可以進行的事項作為結尾：自論文發表以來該主題的發展、其結果如何擴展、推廣或強化，以及其證明如何能更簡潔。README.md總結形式化，而CREDITS.md說明其製作方式：流程、智能體和模型，以及時間和精力（執行記錄）；
• 一個私有的NEXT.md，除非用戶要求，否則絕不發布，它會回答用戶在完成此篇論文後，下一步可以撰寫哪篇論文：幾個候選項目，每個都能自成一篇論文，進行深入探討（障礙、嘗試、證據、已證明的內容），而非一份漸進式擴充的清單；
• 該專案已為Palomar打包，並在用戶許可下，發布並通過Palomar的預檢。

工作分為兩個階段。在第一階段，將論文本身證明的所有內容形式化。論文從文獻中取得的結果可以是暫時的公理。在第二階段，移除這些公理：證明它們，或將那些無法達成的轉為明確的假設。設定在兩個階段之前，而驗證、清理、審計和打包則在之後。

原則

這些原則解釋了以下規則。當沒有規則涵蓋某種情況時，請使用它們。

• 論文是陳述和論證的真理來源；Lean判斷正確性。 與論文不同的陳述，無論其證明多麼乾淨，都是錯誤的形式化。同樣地，透過其他論證達到論文陳述的證明也是如此：形式化檢查的是論文的證明，而不僅僅是其聲明。在任何人證明陳述之前，請對照TeX原始碼審查這些陳述。一旦證明完成，請將其與論文的證明進行比較。永遠不要無聲無息地改變其中任何一個。
• 未經任何人編譯的形式化是草稿。 憑記憶撰寫且從未編譯的Lean程式碼，其引理名稱、型別簽名和輔助引理常常是錯誤的。只要Lean工具鏈可用，就進行編譯。如果沒有工具鏈，或者用戶禁止編譯，就直接說明結果未經驗證。
• 「標準」、「顯然」、「由對稱性」、「常規」仍然需要證明。 Mathlib可能已有此結果；如果沒有，就證明它。只有論文本身從其他來源取得的內容才能成為公理。
• External指的是結果的來源，而非表示它被信任。 被引用的結果因為其來源而存在於External/中。它與其他所有內容一樣需要被證明。
• 假設就是假設，無論其形式為何。 一個未被證明的引用結果就是被假設的，無論它是作為公理、假設還是結構的一個欄位被寫入。不允許使用公理。當陳述的讀者可以看到每個假設時，才允許使用假設，並以其所假設的結果名稱來命名。一個將數據與假設定理混合的結構，會隱藏結果所依賴的內容。一個型別看似數據但實際上包含定理的參數也是如此。
• 數據伴隨其定義性質。 當一個陳述將論文中的一個物件作為參數而非自行建構時，它還必須要求定義該物件的性質。否則，該定理將是關於滿足其他假設的每個物件，這是一個不同的陳述。
• 表示方式的選擇需要橋樑。 Lean的物件可能與論文不同：索引從0而非1開始、列表而非索引族、捆綁的Mathlib結構而非非正式的物件、具體的模型而非「在同構意義下」的描述。當發生這種情況時，證明一個連接兩者的引理，並記錄這個選擇。永遠不要假設兩種表示方式是等價的。
• 常數和範圍是數學的一部分。 冪、因數、取下整、取上整、嚴格與弱不等式、範圍的端點以及ℕ上的截斷減法決定了陳述是否為真。
• 誠實報告。 如果跳過了一步、證明失敗、陳述必須更改、或者證明必須偏離論文，請說明原因。審計只有在可以被信任時才有用。
• 證明中的空白不是虛假的陳述。 當論文的證明使用了其假設未提供的某個事實時，該陳述可能仍然為真。在對該陳述做出任何結論之前，請尋找一個正確的論證。
• 衡量工作。 讀者和註冊表會詢問形式化是如何完成的。隨著進展記錄答案的成本很低，但事後重建則很困難。

規則

• 絕對不要為了讓證明可行而削弱或改變論文結果的陳述。 如果論文的陳述是錯誤的，請立即停止對該結果的工作，並向用戶報告，同時提供反例。在此期間，其他工作可以繼續進行。如果用戶同意，請將最接近的正確版本形式化，並在報告中將其記錄為一個錯誤。明顯的印刷錯誤是唯一的例外（見下文）。

• 絕對不要因為某個證明似乎需要某個假設，就將其添加為論文結果的假設。 添加一個假設會削弱結果。只有在陳述本身有反例時才能添加，而不是因為證明中的某一步失敗了，然後遵循上一條規則。否則，請按照原樣證明該陳述，透過修正的論證，並將證明中的空白記錄為一個E項目。如果你既找不到證明也找不到反例，請告訴用戶缺少什麼。由他們決定是繼續工作，還是將一個較弱的陳述形式化，並記錄為一次偏離。

• 忠實的證明。 使用論文的證明來證明每個結果：相同的中間聲明、相同的建構和情況劃分，以及論文引用它們時的相同早期結果。論文證明所引用的結果構成了它的路線。形式化證明必須具有相同的路線，路線檢查（第6階段）會驗證這一點。只有機制可以不同：策略、關閉常規步驟的Mathlib引理、獨立步驟的順序，以及封裝論文步驟的輔助引理。如果Mathlib恰好能證明某個編號的結果，仍請使用論文的論證來證明它，除非論文本身將其視為已知（它引用了它，或稱其為標準）。

• 僅在必要時才偏離論文的證明，也就是說，出於以下原因且無其他原因：

  1. 論文在該步驟的論證是錯誤的，或者存在空白，並且無法沿其自身思路修復（該步驟也是一個E項目）；
  2. 該步驟需要Lean缺少且專案無法合理建構的數學內容（如同下面關於無法達到的引用結果的情況），而另一個論證可以避免它；
  3. 該步驟在形式化必須使用的某種表示方式中沒有意義（原則），因此對它的忠實翻譯會是一個不同的論證。

  更簡短、更優雅、更通用或更自動化的證明不是理由。更容易形式化或建構速度更快的證明也不是。你發現的簡化論證仍然值得保留：將其記錄下來，並附上草圖，以備報告的「下一步」部分（第8階段）使用，並使用論文的論證來證明該結果。只要理由需要，就偏離多少：修復步驟，而不是整個證明。如果一次偏離會取代某個編號結果的整個論證，而不僅僅是其中一步，請先向用戶提出建議，並說明理由。在此期間，其他工作繼續進行。

• 始終報告每一次偏離。 對於每一次偏離，記錄論文做了什麼、形式化改為做了什麼，以及是哪個理由強制了此更改。記錄在宣告的文件字串中（「對論文的偏離：...」）、在報告的偏離表中、在formalization.yaml（fidelity.divergences）中、在任何隨附文字中、在路線改變時的路線檢查檔案中，以及在下次狀態報告中。任何一處缺少的偏離都是一個缺陷：找到並修復它，就像對待一個被無聲更改的陳述一樣。

• 無法達到的引用結果。 被引用的結果可能需要某個Lean函式庫尚未具備的數學內容。如果在專案中建構這些數學內容是中等工作量，就建構它。否則，預設採用條件形式化：該結果將成為每個使用它的陳述的具名假設。未經詢問即採用預設，並在下次狀態報告中報告。只有當建構缺失的數學內容是龐大但可行的工作量時，才詢問用戶：是否花費這項努力由他們決定。同時，在預設情況下繼續其他工作。如果他們選擇建構它，則將工作分層規劃。每一層都用來自更基礎層的建構和證明替換一些假設，並以一個可以發布的狀態結束。這些假設是唯一可以在沒有反例的情況下被添加到論文結果中的假設。永遠不要將條件形式化呈現為完整形式：其README、formalization.yaml和報告會說明它是條件性的，並列出它所假設的內容。

• 陳述中的小失誤。 如果一個陳述僅因明顯的印刷錯誤（索引錯誤、名稱顛倒、缺少 - 1）而為假，且只能有一種預期解讀，則立即在函式庫和Challenge中將該解讀形式化。在報告和用戶的下次狀態報告中列出每個此類修正。當存在多於一種可能的修正時，將該陳述視為假。

• 一個錯誤的輔助引理（你或某個草稿引入的）需要一個具體的反例，並在可能的情況下在Lean中（decide、norm_num或#eval）進行檢查。然後添加最小的假設，更新其呼叫者，並在提交訊息中記錄此更改。

• 最後，沒有sorry（在Challenge.lean之外）、admit、axiom、native_decide或implemented_by。 native_decide添加了一個公理，Comparator會拒絕它。

• 絕對不要猜測Mathlib的名稱或型別簽名。 在.lake/packages/mathlib中搜索已鎖定的來源，或使用#check、exact?和Loogle。Mathlib經常重新命名和棄用宣告，而棄用警告會指出替代名稱。

• 如果你無法編譯（沒有工具鏈，或用戶禁止），則在未編譯的情況下撰寫Lean。對照鎖定的Mathlib來源檢查每個名稱、型別簽名和導入路徑，保持陳述優先的順序，並將每個結果標記為未經驗證。稍後編譯該專案的人將從第3階段開始。

• 每次每個代碼庫僅運行一個lake build。 同時運行的建構會互相刪除對方的.olean檔案，而在該專案上打開的編輯器會運行其自己的lake setup-file建構。如果你看到「object file … does not exist」，請重試，而不是編輯繞過它。

• 在任何他人可以看到的行動前詢問： 推送、建立儲存庫、變更儲存庫的可見性、開啟或關閉拉取請求、刪除分支、運行Palomar的預檢、提交到Palomar、註冊。其中一項的許可並非其他項目的許可。

• 作者是人。 在README、CREDITS.md和formalization.yaml的automation部分中歸功於AI系統，但絕不能將其作為作者或維護者。

• 從一開始就保留執行記錄（見下方「執行記錄」）。在CREDITS.md、formalization.yaml和狀態報告中報告它。

工作流程

階段	目標	完成條件
0. 設定	記錄任務，提出待解決的問題	設定已記錄
1. 盤點	了解論文：其結果、定義、常數、引用以及它們的證明來源、疑似筆誤	工作檢查清單完整
2. 專案	一個基於Mathlib版本的Lean專案，帶有模組系統，按論文章節佈局	lake build可以運行
3. 陳述	每個定義和編號結果都已陳述，帶有sorry證明；Challenge	陳述已闡明並通過對論文的獨立審查；基準已提交
4. 第一階段	證明論文證明的所有內容，使用論文的證明	僅剩引用結果，作為公理存在於External/中；每次偏離都已報告
5. 第二階段	證明被引用的結果	零公理；每個仍被假設的結果都是一個具名假設
6. 驗證	公理審計、依賴表、路線檢查、Solution和Comparator	scripts/Audit.lean和路線檢查通過；證明已與論文比較；Comparator接受
7. 清理	無警告、無未使用的假設、無誤導性名稱、路線不變	建構僅顯示Challenge的sorry；路線檢查仍然通過
8. 審計	REPORT.md、README.md、CREDITS.md；私有的NEXT.md	每個發現都與TeX原始碼核對；每個後續候選項目都檢查了新穎性並與門檻比較
9. 打包	CI、Palomar檔案和檢查；發布和預檢，經許可	Palomar的本地檢查通過；發布後，預檢報告status: pass

在每個里程碑時提交，提交訊息說明更改了什麼以及原因。

第0階段：設定

記錄這些內容。僅就你無法自行解決的事項詢問用戶：

paper:            arXiv ID和版本（或DOI）；如果有的話，還有TeX原始碼；後續版本...