形式化猜想，再次获陶哲轩认可！
最近，谷歌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 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标签
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/目录
