形式化猜想，再次獲陶哲軒認可！

最近，谷歌DeepMind正式開源了「形式化猜想」GitHub項目，在業(yè)內(nèi)引發(fā)巨大的反響。

項目地址：https://github.com/google-deepmind/formal-conjectures

尤其是，一直以來對此關注度最高的菲爾茲獎得主陶哲軒，發(fā)長文進行了點評。

這一公開數(shù)據(jù)庫將數(shù)學猜想用形式化語言重新表述，讓AI工具能讀懂并嘗試解決這些問題。

目前，這個庫已經(jīng)收錄了一些重量級猜想，比如解析數(shù)論中的4個「蘭道猜想」Landau problem）。

更激動人心的是，DeepMind正向全球數(shù)學家和研究者征集更多猜想，讓這個庫成為一個不斷擴展的「數(shù)學寶庫」。

陶哲軒：AI攻克數(shù)學猜想第一步

你可能好奇，為什么不直接讓AI去解決數(shù)學問題，非要搞什么「形式化」？

這里有個關鍵點：數(shù)學猜想通常是用自然語言描述，對人來說很直觀，但對計算機來說卻像「天書」。

陶哲軒表示，「提出一個數(shù)學猜想容易，證明它卻難如登天」。

若想借助自動化工具在這些問題上取得進展，建立一種標準化的表述形式是關鍵的第一步。

如果直接讓AI去處理這些模糊的表述，它很可能只是在技術細節(jié)上「鉆空子」。

舉個栗子，AI可能構(gòu)造出一個正式陳述，但其包含了一個原本并非意圖中的邊界情況，如把關鍵參數(shù)設為零，繞過真正的問題，從而給出一個看似正確但毫無意義的答案。

形式化的意義，就在于把這些模糊的表述變成「精確無誤」的數(shù)學語言。

只有這樣，AI才能真正理解問題，嘗試給出有意義的解答。DeepMind的這個庫，就是為AI提供這樣的「標準答案模板」。

接下來，一起看看這個庫中都有哪些要點。

數(shù)學猜想庫上線，破解世紀難題鑰匙

GitHub項目主頁中介紹，形式化猜想——一份使用mathlib在Lean中形式化表述的猜想集合。

目標

盡管包含證明的形式化定理庫日益增長，但僅陳述形式化的開放猜想仍十分匱乏。填補這一空白將具有多重意義：

? 為自動定理證明器和形式化工具提供優(yōu)質(zhì)基準測試集

? 通過形式化澄清猜想的精確含義

? 通過突顯缺失定義，促進mathlib的擴展

形式化準確性  

無證明的數(shù)學陳述形式化具有固有挑戰(zhàn)性，原始猜想的微妙之處可能在形式化表述中失真。為緩解該問題，DeepMind將采取兩項措施：

1 對貢獻內(nèi)容進行嚴格人工審核

2 定期使用AlphaProof識別潛在錯誤形式化

如何參與貢獻  

DeepMind在此誠邀各方大佬前來貢獻，每個人可添加最喜愛的猜想（或創(chuàng)建issue描述）。

貢獻方式  

本倉庫接受多種形式的貢獻：

1. 新增問題形式化

不同于千禧難題、斯梅爾問題列表等傳統(tǒng)猜想集，本倉庫鼓勵多元來源的貢獻，包括但不限于：

• 數(shù)學教材
• 研究論文（含arXiv預印本）
• MathOverflow提問
• 專題問題集（如埃爾德什問題、維基百科未解決問題列表、蘇格蘭咖啡館問題集等）

2. 提交形式化需求，創(chuàng)建issue時請?zhí)峁?/span>

• 可靠參考文獻鏈接
• 精確的非形式化猜想陳述

3. 完善現(xiàn)有內(nèi)容

• 補充參考文獻指針
• 增加AMS數(shù)學主題分類標簽

4. 修正錯誤形式化

提交PR修復錯誤或創(chuàng)建issue指正問題

用法、結(jié)構(gòu)與特性

這是一個基于lake管理、依賴mathlib的Lean 4項目。使用前需安裝：

1. elan + lake + Lean

2.（可選）VSCode及相關插件

初始化命令：

lake exe cache get
lake build

目錄結(jié)構(gòu)  

按猜想來源類型組織，包含兩個特殊目錄：

• Util/：存放工具組件? 分類屬性標簽系統(tǒng)? answer() elaborator? 代碼檢查器
• ForMathlib/：可向上游提交至mathlib的代碼（遵循mathlib目錄結(jié)構(gòu)）

核心特性  

1. 分類屬性標簽

用于標記問題陳述的類別，當前支持：

• research open：學界未解決的數(shù)學問題
• research solved：學界已公認解決的問題（不要求形式化證明）
• graduate：研究生級別問題
• undergraduate：本科級別問題
• high_school：中學級別問題
•  API：圍繞新定義的基礎理論構(gòu)建
• test：用于測試定義的「單元測試」

使用示例：

@[category research open]
theorem foo : Transcendental ? (rexp 1 + π) := by sorry
@[category research solved]
theorem bar : FermatLastTheorem := by sorry

2. AMS數(shù)學主題標簽

采用AMS MSC2020主分類號標注數(shù)學領域，例如：

@[AMS 11] -- "數(shù)論"分類
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()中提供項及證明不意味問題已解決
• 答案的數(shù)學意義評估不在本倉庫范疇內(nèi)

風格規(guī)范

1. 文件組織

• 每個問題獨立成文件（變體與特例可合并）
• 維基百科來源的問題應置于FormalConjectures/Wikipedia/

2. 定義與API

• 允許自定義定義（需有助于闡明問題）
• 鼓勵為定義提供基礎API以驗證行為

3. 陳述格式

• 基準問題使用theorem聲明
• 測試用例優(yōu)先使用example
• 必須包含至少一個AMS標簽

4. 問題轉(zhuǎn)譯

• 英語疑問句形式：

/-- 原文："Does P hold ?" -/
theorem myConjecture : P ? answer(sorry) := by sorry

• 已解決問題替換為answer(True/False)
• ·非疑問句形式：

/-- 原文："P holds" -/
theorem myConjecture : P := by sorry

• 反例情況應陳述為? P

版本

• 跟蹤mathlib月度發(fā)布版本（而非master分支）
• 若問題需mathlib未收錄的定義，可暫存于ForMathlib/目錄