DeepMind首個猜想庫開源，獲陶哲軒力挺！
形式化猜想，再次獲陶哲軒認可！
最近，谷歌DeepMind正式開源了「形式化猜想」GitHub項目，在業內引發巨大的反響。
項目地址：https://github.com/google-deepmind/formal-conjectures
尤其是，一直以來對此關注度最高的菲爾茲獎得主陶哲軒，發長文進行了點評。
這一公開數據庫將數學猜想用形式化語言重新表述，讓AI工具能讀懂并嘗試解決這些問題。
目前，這個庫已經收錄了一些重量級猜想，比如解析數論中的4個「蘭道猜想」Landau problem）。
更激動人心的是，DeepMind正向全球數學家和研究者征集更多猜想，讓這個庫成為一個不斷擴展的「數學寶庫」。
陶哲軒：AI攻克數學猜想第一步
你可能好奇，為什么不直接讓AI去解決數學問題，非要搞什么「形式化」？
這里有個關鍵點：數學猜想通常是用自然語言描述，對人來說很直觀，但對計算機來說卻像「天書」。
陶哲軒表示，「提出一個數學猜想容易，證明它卻難如登天」。
若想借助自動化工具在這些問題上取得進展，建立一種標準化的表述形式是關鍵的第一步。
如果直接讓AI去處理這些模糊的表述，它很可能只是在技術細節上「鉆空子」。
舉個栗子，AI可能構造出一個正式陳述，但其包含了一個原本并非意圖中的邊界情況，如把關鍵參數設為零，繞過真正的問題，從而給出一個看似正確但毫無意義的答案。
形式化的意義，就在于把這些模糊的表述變成「精確無誤」的數學語言。
只有這樣，AI才能真正理解問題，嘗試給出有意義的解答。DeepMind的這個庫，就是為AI提供這樣的「標準答案模板」。
接下來，一起看看這個庫中都有哪些要點。
數學猜想庫上線，破解世紀難題鑰匙
GitHub項目主頁中介紹，形式化猜想——一份使用mathlib在Lean中形式化表述的猜想集合。
目標
盡管包含證明的形式化定理庫日益增長，但僅陳述形式化的開放猜想仍十分匱乏。填補這一空白將具有多重意義：
? 為自動定理證明器和形式化工具提供優質基準測試集
? 通過形式化澄清猜想的精確含義
? 通過突顯缺失定義，促進mathlib的擴展
形式化準確性
無證明的數學陳述形式化具有固有挑戰性，原始猜想的微妙之處可能在形式化表述中失真。為緩解該問題，DeepMind將采取兩項措施：
1 對貢獻內容進行嚴格人工審核
2 定期使用AlphaProof識別潛在錯誤形式化
如何參與貢獻
DeepMind在此誠邀各方大佬前來貢獻，每個人可添加最喜愛的猜想（或創建issue描述）。
貢獻方式
本倉庫接受多種形式的貢獻：
1. 新增問題形式化
不同于千禧難題、斯梅爾問題列表等傳統猜想集，本倉庫鼓勵多元來源的貢獻，包括但不限于：
- 數學教材
- 研究論文（含arXiv預印本）
- MathOverflow提問
- 專題問題集（如埃爾德什問題、維基百科未解決問題列表、蘇格蘭咖啡館問題集等）
2. 提交形式化需求，創建issue時請提供：
- 可靠參考文獻鏈接
- 精確的非形式化猜想陳述
3. 完善現有內容
- 補充參考文獻指針
- 增加AMS數學主題分類標簽
4. 修正錯誤形式化
提交PR修復錯誤或創建issue指正問題
用法、結構與特性
這是一個基于lake管理、依賴mathlib的Lean 4項目。使用前需安裝：
1. elan + lake + Lean
2.（可選）VSCode及相關插件
初始化命令：
lake exe cache get
lake build目錄結構
按猜想來源類型組織，包含兩個特殊目錄：
Util/：存放工具組件? 分類屬性標簽系統?answer()elaborator? 代碼檢查器ForMathlib/：可向上游提交至mathlib的代碼（遵循mathlib目錄結構）
核心特性
1. 分類屬性標簽
用于標記問題陳述的類別，當前支持：
research open：學界未解決的數學問題research solved：學界已公認解決的問題（不要求形式化證明）graduate：研究生級別問題undergraduate：本科級別問題high_school：中學級別問題-
API：圍繞新定義的基礎理論構建 test：用于測試定義的「單元測試」
使用示例：
@[category research open]
theorem foo : Transcendental ? (rexp 1 + π) := by sorry
@[category research solved]
theorem bar : FermatLastTheorem := by sorry2. AMS數學主題標簽
采用AMS MSC2020主分類號標注數學領域，例如：
@[AMS 11] -- "數論"分類
theorem flt : FermatLastTheorem := by sorry? 在Lean文件中可用#AMS命令查看所有可選值
? VSCode中懸停標簽可顯示對應學科
? 支持多標簽組合：@[AMS foo bar]
3. answer() elaborator
用于需用戶提供答案的開放問題（如Hadwiger-Nelson問題）：
@[category research open]
theorem HadwigerNelsonProblem :
IsLeast {n : ? | ExistsColoring n} answer(sorry) := by sorry重要說明
- 在
answer()中提供項及證明不意味問題已解決 - 答案的數學意義評估不在本倉庫范疇內
風格規范
1. 文件組織
- 每個問題獨立成文件（變體與特例可合并）
- 維基百科來源的問題應置于
FormalConjectures/Wikipedia/
2. 定義與API
- 允許自定義定義（需有助于闡明問題）
- 鼓勵為定義提供基礎API以驗證行為
3. 陳述格式
- 基準問題使用
theorem聲明 - 測試用例優先使用
example - 必須包含至少一個AMS標簽
4. 問題轉譯
- 英語疑問句形式：
/-- 原文："Does P hold ?" -/
theorem myConjecture : P ? answer(sorry) := by sorry- 已解決問題替換為
answer(True/False) - ·非疑問句形式：
/-- 原文："P holds" -/
theorem myConjecture : P := by sorry- 反例情況應陳述為
? P
版本
- 跟蹤mathlib月度發布版本（而非master分支）
- 若問題需mathlib未收錄的定義，可暫存于
ForMathlib/目錄
