摘要
数学正在迎来 AI 革命。 最近几个月尤为明显。比如，就在前几天，Google DeepMind 新论文宣布其最新系统 AlphaProof Nexus 在一次自主运行中，解决了 353 道开放 Erdős 问题中的 9 道，其中两道已在数学界悬而未决长达 56 年，并且每道题的推理成本，仅需区区几百美元。详情可参阅《一个问题几百美元，DeepMind 智能体一次搞定了 9 个 Erdős 问题》。 Erdős 问题通常指匈牙利传奇数学家 Paul Erdős 在其一生中提出的大量公开数学问题与猜想。这些问题广泛分布于组合数学、数论、图论、离散几何、概率论等领域，其中许多长期未解，并被视为相关方向的重要研究基准与前沿挑战。这一结果之所以可信，关键在于 AlphaProof Nexus 并非生成自然语言证明，而是将大语言模型（Gemini 3.1 Pro）与形式化验证工具 Lean 深度结合：AI 提出证明，Lean 逐步核查每一个逻辑步骤，通不过就直接拒绝。所有证明代码已公开于 GitHub，任何人都可以独立复现验证。 现在，新的进展来了！Meta 联合纽约大学等机构正式发布了 ATLAS（Autoformalized Textbook Library At Scale），一项迄今为止规模最大的自动化数学形式化工程之一。 项目论文和代码都已发布。 项目地址：https://github.com/facebookresearch/atlas-lean/ 论文地址：https://github.com/facebookresearch/atlas-lean/blob/main/formalizing_mathematics_at_scale.pdf 什么是 ATLAS？ 简单来说，ATLAS 是一个基于 Lean 4 的数学形式化代码库，其核心目标是：将数学教科书中的非正式定理陈述与证明，自动翻译成计算机可逐行验证的形式化代码。 这件事听起来枯燥，但意义深远。Lean 是一种「证明助手」语言，当你向它提交一段数学证明时，它会像编译器检查代码那样，逐步验证每一个推导步骤的逻辑合法性。是的，只要 Lean 通过，这个证明就在形式意义上无懈可击。