我是如何「憑感覺」證明康威精煉猜想的

重點摘要

Dan Abramov 利用 Claude、ChatGPT 和 Codex 代理程式來生成、審核並將康威（Conway）關於全能整數（omnific integers）的精煉猜想進行 Lean 形式化證明；該證明通過了機械檢查，但尚未經過獨立驗證。

---

康威猜想的內容

康威的精煉猜想主張，對於任何全能整數（omnific integers）的乘積等式 (a b = c d)，都存在整數 (e,f,g,h) 使得：

• (a = e f)
• (b = g h)
• (c = e g)
• (d = f h)

換句話說，任何全能整數的兩種因式分解都承認一個共同的精煉，這反映了基本整數的一個性質，即乘積可以分解為質因數並重新組合。

AI 驅動的研究流程

1. 問題選擇

• Claude 被要求挑選一個超現實數（surreal numbers）領域的未解問題。它選擇了精煉猜想，並引用了 L’Innocente 和 Mantova 最近的研究，該研究將此猜想簡化為關於 (K((\mathbb{R}^{\le 0}))) 中不可約元素的陳述。
• 作者指出，Claude 的簡化並不完整，但由於該問題與 ONAG 出版 50 週年的情感連結，它仍然具有吸引力。

2. 早期的單次嘗試

• 最初的提示詞要求 Claude「做出突破」。模型產生了難以驗證且充滿術語的混亂文字。
• 切換到 ChatGPT（稱為 Sol）後，雖然提出了較為謙遜的說法，但仍需要大量的人工審核。

3. 多代理實驗室 (Codex)

• 一個 專案經理 (PM) 代理協調工作流程。
• 兩個 數學 代理生成候選引理。
• 一個 紅隊 (Red) 代理嘗試尋找漏洞。
• 一個 隨機 (Random) 代理探索邊緣想法。
• 一個 Lean 代理將有希望的結果轉換為 Lean 程式碼。
• 代理們透過一個「自助餐廳」聊天室進行溝通，在保持角色邊界的同時實現了交叉激盪。

4. Token 消耗與成本

• 大約處理了 400 億個 token，其中約 2.1 億個為輸出。
• 預估 API 成本：≈ 40,000 美元。

關鍵里程碑

週次	里程碑	結果
1	問題框架與初步提示	Claude 產生了模糊的問題陳述；ChatGPT 提供了關鍵的「懷疑」聲音。
2	使用 Codex 代理建立實驗室	生成了數十份草稿「論文」；許多包含發明的術語和邏輯漏洞。
3	首次死胡同與失敗的「引導」證明	ChatGPT 聲稱已完全證明，但新的對話視窗揭露了循環論證。
4	透過修正錯字進行基準測試	模型發現了同行評審參考文獻中的錯誤並經作者確認，增強了信心。
5	燒毀與挽救策略	丟棄了大部分嘈雜的草稿，保留了關於 Hahn 級數中 有限度素數性 的連貫結果。
6	形式化驗證	兩個獨立的 Lean 代理驗證了有限度結果，隨後驗證了完整的精煉猜想。
7	證明映射工具	自訂腳本生成了 Mermaid 圖表和互動式網頁 UI，以視覺化依賴結構。

最終的 Lean 證明

• 證明位於 GitHub 儲存庫 gaearon/conway-refinement 中的 ConwayRefinement/Standalone 目錄下。
• 每個獨立檔案僅匯入 Mathlib，確保了陳述的自給自足。
• 審核驗證：
  • 未引入額外的公理。
  • 匯入符合獨立政策。
  • 每個陳述都有配對的 Lean 證明。
• 由 Lean 核心編譯的 證明證書 確認了該猜想的陳述（參見連結的編譯影片）。

學到的教訓

1. 感覺 vs. 理解 – 該專案在沒有深厚個人專業知識的情況下取得成功，但需要不斷進行「感覺檢查」以檢測偏差。
2. 代理紀律 – 用於背景形式化和新結果的獨立 Lean 代理防止了穩定程式碼的污染。
3. 審核基礎設施 – 獨立資料夾、模組層級檢查和公理檢查器對於審閱者的信任至關重要。
4. 人類回饋 – 就錯字修正與數學家進行電子郵件溝通，提供了現實檢驗並建立了可信度。
5. 模型互補性 – Claude 擅長結構化的 Lean 生成；ChatGPT 更擅長探索性數學和批判。
6. Token 經濟學 – 更具引導性的工作流程可以將成本降低 5 到 10 倍。
7. 證明呈現 – 將 Lean 程式碼轉換為可讀的 PDF 仍然是一個瓶頸；互動式證明映射有助於彌補這一差距。

社群反應（精選 HN 評論）

「這種方法感覺就像巫術與魔法之間的區別；作者召喚了強大的存在（LLM）卻沒有完全理解咒語。」 – @gbjcantab

「我不是數學家。『在每個間隙中生成』的規則是如何讓你超越有理數的？」 – @rlue

「這個工作流程反映了現實世界的工程過程：多代理、對抗性測試和持續整合。」 – @spongebobstoes

「證明令人印象深刻，但如果沒有獨立驗證，數學界仍將保持懷疑。」 – @patcon（連結至一位教授的評論）。

開放性問題

• 驗證 – 獨立數學家需要審核 Lean 程式碼並確認邏輯步驟。
• 簡化 – 目前證明長度較大；未來的工作可能會使用生成的證明映射來壓縮它。
• 推廣 – 同樣的多代理流程能否應用於其他未解問題而無需領域專業知識？
• 模型對齊 – LLM 提供者如何在不鼓勵「幻覺」定理的情況下，更好地支援嚴謹的數學研究？

---

作者歡迎對證明儲存庫和 Zulip 頻道進行批評、錯誤報告和討論。