形式化猜想，再次获陶哲轩认可！

最近，谷歌DeepMind正式开源了「形式化猜想」GitHub项目，在业内引发巨大的反响。

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

尤其是，一直以来对此关注度最高的菲尔兹奖得主陶哲轩，发长文进行了点评。

这一公开数据库将数学猜想用形式化语言重新表述，让AI工具能读懂并尝试解决这些问题。

目前，这个库已经收录了一些重量级猜想，比如解析数论中的4个「兰道猜想」Landau problem）。

更激动人心的是，DeepMind正向全球数学家和研究者征集更多猜想，让这个库成为一个不断扩展的「数学宝库」。

你可能好奇，为什么不直接让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 getlake 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 sorry

2. 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标签

5. 问题转译

· 英语疑问句形式：

/-- 原文："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/目录