炒股就看金麒麟分析師研報，權威，專業，及時，全面，助您挖掘潛力主題機會！
新智元報道
編輯：桃子
【新智元導讀】谷歌DeepMind重磅出擊，開源首個形式化數學猜想庫，獲陶哲軒力挺！從解析數論的蘭道猜想開始，這個開源項目將為AI破解數學難題的未來鋪路。
形式化猜想，再次獲陶哲軒認可！
最近，谷歌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及相關插件
初始化命令：
目錄結構
按猜想來源類型組織，包含兩個特殊目錄：
·Util/：存放工具組件• 分類屬性標籤系統•answer()elaborator• 代碼檢查器
·ForMathlib/：可向上游提交至mathlib的代碼（遵循mathlib目錄結構）
核心特性
1. 分類屬性標籤
用於標記問題陳述的類別，當前支持：
·research open：學界未解決的數學問題
·research solved：學界已公認解決的問題（不要求形式化證明）
·graduate：研究生級別問題
·undergraduate：本科級別問題
·high_school：中學級別問題
·API：圍繞新定義的基礎理論構建
·test：用於測試定義的「單元測試」
使用示例：
2. AMS數學主題標籤
採用AMS MSC2020主分類號標註數學領域，例如：
• 在Lean文件中可用#AMS命令查看所有可選值
• VSCode中懸停標籤可顯示對應學科
• 支持多標籤組合：@[AMS foo bar]
3.answer()elaborator
用於需用戶提供答案的開放問題（如Hadwiger-Nelson問題）：
重要說明
· 在answer()中提供項及證明不意味問題已解決
· 答案的數學意義評估不在本倉庫範疇內
風格規範
1. 文件組織
· 每個問題獨立成文件（變體與特例可合併）
· 維基百科來源的問題應置於FormalConjectures/Wikipedia/
2. 定義與API
· 允許自定義定義（需有助於闡明問題）
· 鼓勵為定義提供基礎API以驗證行為
3. 陳述格式
· 基準問題使用theorem聲明
· 測試用例優先使用example
· 必須包含至少一個AMS標籤
5. 問題轉譯
· 英語疑問句形式：
· 已解決問題替換為answer(True/False)
· 非疑問句形式：
· 反例情況應陳述為¬ P
版本
· 跟蹤mathlib月度發布版本（而非master分支）
· 若問題需mathlib未收錄的定義，可暫存於ForMathlib/目錄
參考資料：
https://mathstodon.xyz/@tao/114586574834318736
GitHub - google-deepmind/formal-conjectures: A collection of formalized statements of conjectures in