闻乐 发自 凹非寺

量子位 | 公众号 QbitAI

陶哲轩转发，AI搞数学证明的标准习题集来了！

DeepMind最新开源形式化数学猜想库——

猜想库收录了经典的形式化表述的数学猜想集合，例如，解析数论中的四个朗道问题。

不仅如此，资源库中还提供了各种代码函数，以方便用户对自然语言的数学猜想进行形式化的表述。

陶哲轩曾用Lean形式化证明了PFR猜想（多项式Freiman-Ruzsa猜想），这项成就的第一步就是将猜想的核心概念转化为计算机可验证的形式化版本。

目前，这位“数学界的计算机推广大神”已转发此项目，并表示：

“如果希望利用自动化工具帮助开放性问题，那么对这些问题进行形式化表述是重要的第一步。”

DeepMind的形式化数学猜想库一经建成，团队就表示所有人都可以将数学猜想添加到资源库中，呼吁大家积极参与。

感兴趣的数学家们可以行动起来了。

形式化数学猜想库有什么用

虽然带证明的形式化定理语料库不断扩充，但仅陈述开放式猜想的形式化资源却十分稀缺。

这类资源有望成为自动定理证明或形式化工具的测试基准，来帮助AI模型提升数学推理及证明能力。

DeepMind此次开源的猜想库在一定程度上缓解了这个问题。

它收录了使用Lean形式化表述的数学猜想集合，这些猜想来源于各个途径，并且类型多样。

下图展示了题目类别统计。

这个猜想库相当于为计算机写了一套形式化的“习题集”，还是能够随时扩充并且自带审核的那种！

有了这个“习题集”，传统ATP（自动推理证明）就可以直接基于里面的命题进行证明搜索，比如使用归结法尝试推导矛盾或验证等。

除此之外，将猜想库作为训练数据，就能让模型学习数学猜想的模式，AI就有可能提出新猜想。

例如，AlphaGeometry（DeepMind开发的专门用于自动解决奥林匹克几何题的AI系统）就能够依赖合成几何猜想训练模型。

可以说，形式化数学猜想库是AI+ATP范式的关键前置步骤。

目前，该猜想库刚刚起步，团队希望更多人能参与其中，丰富猜想库的内容。

所有感兴趣的用户都可以通过以下这几种方式参与其中：

1. 添加新的问题形式化：猜想可以来自各种地方，包括数学教科书、研究论文、专用问题列表等。

2. 提出你希望的形式化问题：建议包含参考文献链接和精确的非正式表述。

3. 改进问题的引用和标记：为现有命题添加参考文献或补充AMS学科分类标签。

4. 修复错误的形式化：鼓励通过提交PR修复不准确的表述，或提交issue反馈潜在缺陷。

那么如何操作呢？

接下来，让我们给大家解答。

流程大致分为这样几个步骤：

首先，你要在在GitHub上创建问题，清晰描述计划贡献的内容，包括对要添加的数学猜想的概述、相关背景信息以及自己对该猜想的初步理解等，然后将问题分配给自己，以便跟踪和管理贡献进度。

并且，可以从官方仓库Fork一份到自己的GitHub账户下进行修改。

然后，按照仓库的目录结构和组织方式，确定猜想应该放置的具体的位置，再将你的形式化猜想添加到适当的文件/目录结构中。

下一步就是在本地运行lake build命令，避免出现语法错误或其他导致系统无法正常运行的问题，确保添加或修改后的代码能够成功构建。

完成上述步骤就可以向官方仓库提交拉取请求了，随后等待即可～

DeepMind与陶哲轩

说来，陶哲轩与DeepMind也是互动颇多。

早在2023年，DeepMind提出FunSearch——一种能够为数学和计算机科学问题搜索解决方案的方法。

陶哲轩就曾称赞FunSearch是“利用LLM进行数学发现的有前途的范式”。

该方法首次证明LLMs可以生成用计算机代码编写的函数，相关工作发表在《Nature》杂志上。

就在前不久，谷歌DeepMind与陶哲轩等一众顶尖科学家一起共同打造了——一个LLM驱动的进化编码Agent，用于通用算法的发现与优化。

几百年未曾解决的几何挑战接吻数（Kissing Number）问题，也都因为它的出现前进了一大步。

它发现了一个由593个外球体组成的结构，直接刷新了11维空间中的下限。

AlphaEvolve团队将其应用于数学分析、几何学、组合学和数论等多个领域。

在大约75%的案例中，它能够重新发现最先进的解决方案。

在20%的案例中，它改进了之前已知的最佳解决方案。

可以说，这是AI与数学的一次里程碑式碰撞。