陶哲轩转发AI数学习题集DeepMind开源数学标准题库
DeepMind最近开源了一个面向AI的数学猜想题库，陶哲轩第一时间转发支持。这个项目收录了大量尚未被证明的数学猜想，并用Lean语言进行了形式化处理——也就是转化成计算机能理解的语言。
这个操作的意义在哪？
- 对AI来说，这是“标准题库”。可以用来训练模型如何理解数学猜想。
- 对数学家来说，这是个合作平台。可以添加、修正猜想，或作为自动定理证明（ATP）的实验场。
- 对整个人类数学社区来说，这是一套未来AI协作式数学研究的“基础设施”。
为什么要做“形式化”？这其实是让问题变得可验证、可编程。陶哲轩自己就曾用Lean形式化语言完成PFR猜想的验证，他也强调：“这是走向AI协助解决数学难题的第一步。”
目前，这个题库刚起步，DeepMind鼓励大家贡献新猜想、补充引用、修正格式错误等。流程也很友好：在GitHub上创建issue、fork代码库、加入你的猜想、跑一下lake build确保无误，就能提交拉取请求了。
不仅是题库，DeepMind还表示未来会结合自己的AI证明系统AlphaProof一起用，让AI自己“找题+解题”。这逻辑一旦跑通，AI辅助发现数学新定理也就不远了。
项目地址：github.com/google-deepmind/formal-conjectures
在线浏览：
