形式化猜想，再次獲陶哲軒認(rèn)可！

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

項(xiàng)目地址：https://github.com/google-deepmind/formal-conjectures

尤其是，一直以來對(duì)此關(guān)注度最高的菲爾茲獎(jiǎng)得主陶哲軒，發(fā)長(zhǎng)文進(jìn)行了點(diǎn)評(píng)。

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

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

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

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

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

這里有個(gè)關(guān)鍵點(diǎn)：數(shù)學(xué)猜想通常是用自然語(yǔ)言描述，對(duì)人來說很直觀，但對(duì)計(jì)算機(jī)來說卻像「天書」。

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

若想借助自動(dòng)化工具在這些問題上取得進(jìn)展，建立一種標(biāo)準(zhǔn)化的表述形式是關(guān)鍵的第一步。

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

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

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

只有這樣，AI才能真正理解問題，嘗試給出有意義的解答。DeepMind的這個(gè)庫(kù)，就是為AI提供這樣的「標(biāo)準(zhǔn)答案模板」。

接下來，一起看看這個(gè)庫(kù)中都有哪些要點(diǎn)。

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

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

目標(biāo)

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

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

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

? 通過突顯缺失定義，促進(jìn)mathlib的擴(kuò)展

形式化準(zhǔn)確性  

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

1 對(duì)貢獻(xiàn)內(nèi)容進(jìn)行嚴(yán)格人工審核

2 定期使用AlphaProof識(shí)別潛在錯(cuò)誤形式化

如何參與貢獻(xiàn)  

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

貢獻(xiàn)方式  

本倉(cāng)庫(kù)接受多種形式的貢獻(xiàn)：

1. 新增問題形式化

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

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

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

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

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

• 補(bǔ)充參考文獻(xiàn)指針
• 增加AMS數(shù)學(xué)主題分類標(biāo)簽

4. 修正錯(cuò)誤形式化

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

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

這是一個(gè)基于lake管理、依賴mathlib的Lean 4項(xiàng)目。使用前需安裝：

1. elan + lake + Lean

2.（可選）VSCode及相關(guān)插件

初始化命令：

lake exe cache get
lake build

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

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

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

核心特性  

1. 分類屬性標(biāo)簽

用于標(biāo)記問題陳述的類別，當(dāng)前支持：

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

使用示例：

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

2. AMS數(shù)學(xué)主題標(biāo)簽

采用AMS MSC2020主分類號(hào)標(biāo)注數(shù)學(xué)領(lǐng)域，例如：

@[AMS 11] -- "數(shù)論"分類
theorem flt : FermatLastTheorem := by sorry

? 在Lean文件中可用#AMS命令查看所有可選值

? VSCode中懸停標(biāo)簽可顯示對(duì)應(yīng)學(xué)科

? 支持多標(biāo)簽組合：@[AMS foo bar]

3. answer() elaborator

用于需用戶提供答案的開放問題（如Hadwiger-Nelson問題）：

@[category research open]
theorem HadwigerNelsonProblem :
    IsLeast {n : ? | ExistsColoring n} answer(sorry) := by sorry

重要說明

• 在answer()中提供項(xiàng)及證明不意味問題已解決
• 答案的數(shù)學(xué)意義評(píng)估不在本倉(cāng)庫(kù)范疇內(nèi)

風(fēng)格規(guī)范

1. 文件組織

• 每個(gè)問題獨(dú)立成文件（變體與特例可合并）
• 維基百科來源的問題應(yīng)置于FormalConjectures/Wikipedia/

2. 定義與API

• 允許自定義定義（需有助于闡明問題）
• 鼓勵(lì)為定義提供基礎(chǔ)API以驗(yàn)證行為

3. 陳述格式

• 基準(zhǔn)問題使用theorem聲明
• 測(cè)試用例優(yōu)先使用example
• 必須包含至少一個(gè)AMS標(biāo)簽

4. 問題轉(zhuǎn)譯

• 英語(yǔ)疑問句形式：

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

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

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

• 反例情況應(yīng)陳述為? P

版本

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