陶哲轩转发！DeepMind开源「AI数学证明标准习题集」

88 0 0

文章摘要

DeepMind最新开源形式化数学猜想库，该库由陶哲轩转发，具有重要意义。猜想库收录了经典的形式化表述的数学猜想集合，如解析数论中的四个朗道问题，还提供代码函数方便用户对自然语言的数学猜想进行形式化表述。陶哲轩曾用Lean形式化证明了PFR猜想，他认为对开放性问题进行形式化表述是利用自动化工具的重要第一步。

形式化数学猜想库作用显著。目前仅陈述开放式猜想的形式化资源稀缺，而该猜想库在一定程度上缓解了这一问题。它收录使用Lean形式化表述的多样数学猜想，相当于为计算机提供了可扩充且自带审核的“习题集”。传统ATP可基于其中命题进行证明搜索，将其作为训练数据能让模型学习数学猜想模式，使AI有可能提出新猜想，是AI + ATP范式的关键前置步骤。

该猜想库刚起步，团队希望更多人参与。用户可通过添加新的问题形式化、提出希望的形式化问题、改进问题的引用和标记、修复错误的形式化等方式参与。操作流程大致为：先在GitHub上创建问题并分配给自己，从官方仓库Fork一份到自己账户下修改；接着确定猜想放置位置并添加到适当文件/目录结构；再在本地运行lake build命令确保代码能成功构建；最后提交拉取请求等待审核，猜想库会通过人工审核和AlphaProof辅助识别错误。

DeepMind与陶哲轩互动颇多。2023年DeepMind提出的FunSearch获陶哲轩称赞，其相关工作发表在《Nature》杂志。前不久，谷歌DeepMind与陶哲轩等打造AlphaEvolve，推动了几百年未解决的几何挑战接吻数问题，在多个领域应用成果显著，约75%案例能重新发现最先进解决方案，20%案例改进了之前最佳方案。陶哲轩表示AlphaEvolve的数学潜力仍在开发中，值得期待更多进展。