数学中国

标题: AI 为什么突然会做“数学研究” [打印本页]

作者: luyuanhong 时间: 2026-10-25 11:38
标题: AI 为什么突然会做“数学研究”
AI 为什么突然会做“数学研究”

原创 eric AICG 果园 2026 年 10 月 13 日 20:59 广东

Two Minute Papers 解读 “ OpenAI 刚刚重新定义了“做数学”的含义” ——看懂 OpenAI Astra 背后的技术逻辑（ https://www.youtube.com/watch?v=z_sXLlLVUls ）

这支视频真正值得关注的，不是“ AI 解出了十道数学题”，而是 AI 开始进入了数学研究最核心的一段流程：提出思路、反复修改、写成证明，并交给形式化系统逐步验算。

这和让 ChatGPT 算一道积分，根本不是同一件事。

2026 年 8 月，OpenAI 公布了十项数学与理论计算机科学结果，涉及高维球体堆积、编码理论、群论、量子复杂性、格密码学和图论等方向。其中有些是解决长期开放问题，有些是对已有问题给出重要推进。OpenAI 表示，这些结果由其内部版本的 Astra 模型生成；随后研究人员协助整理成论文，并将证明形式化为 Lean 代码。

要理解它的意义，可以把这套系统拆成四层。

第一层：模型不再只“回答”，而是在搜索证明路径

普通聊天模型面对数学题，往往像一个很会写答案的学生：它能复述定义、模仿证明格式，也能给出看似合理的推导。但一旦步骤变长，就容易在某一个小地方悄悄出错，最后仍然写得很自信。

研究级数学的问题难点不只是计算，而是没有人告诉你正确路径。你需要不断尝试：

● 有没有一个能把问题换成另一个问题的表示法？

● 某个引理是否足以推出结论？

● 这个构造会不会在边界条件下失败？

● 一条路走不通时，究竟是计算错了，还是方向错了？

公开的“推理过程详解”显示，这些成果并非每次一击命中：模型会经历失败方案、发现障碍、改变问题视角，再把新的结构组织成完整论证。

所以，更准确的比喻不是“ AI 背了很多数学题”，而是：它正在把大量已学到的数学工具重新组合，在可验证的约束下搜索一条以前没人写出的路。

第二层：数学特别适合给 AI 做“反馈训练”

为什么 AI 先在数学上显得强大，而不是先解决所有科学问题？

一个重要原因是：数学有很强的对错反馈。

如果模型声称一个等式成立，可以代入检验；如果它构造了反例，可以检查反例是否满足条件；如果它写出一个证明，可以把每一个推理步骤交给形式化系统检查。这样的反馈比“这篇文章写得是否有洞见”“这个商业决策是否正确”清晰得多。

这让 AI 可以在大量尝试中淘汰明显错误的路径，把更多计算资源留给有希望的方向。OpenAI 在后续 Astra 介绍中只公开了高层信息：模型结合了预训练、强化学习和对齐方面的研究；但没有公开其完整架构、训练数据、奖励函数或搜索策略。

因此，我们能确定的是“它做到了怎样的流程”，不能确定“它内部到底用了哪一种神秘算法”。把未公开的工程细节说成事实，是不严谨的。

第三层：Lean 让“看起来对”变成“机器逐步核过”

这次发布最关键的一部分，是 Lean 。

Lean 是一种形式化证明语言。人类常见的数学证明会省略许多步骤，例如“显然”“类似可得”“由标准结论可知”。数学家读得懂，但计算机无法凭直觉补全。

在 Lean 里，你要把定义、前提、引理和推理步骤写得足够精确，让系统能逐步检查：这一步是否真的能从前面的内容推出下一步。

可以把它想成两种不同的标准：

● 人类论文：专家读后觉得论证合理；

● Lean 证明：检查器确认每一个被写明的推理都符合规则。

OpenAI 发布了十项结果对应的 Lean 4 形式化文件，并提供独立构建方式。任何有相应环境的人都可以下载并运行检查，而不必只相信发布者的口头说明。

这一步非常重要，因为语言模型最危险的能力之一，就是能够写出“像真的一样”的错误论证。形式化验证并不让模型自动拥有真理，但它为模型输出加了一道极其严格的闸门。

第四层：这仍不是“ AI 独立完成了全部数学”

看到 Lean 以后，也不能得出“以后数学家没有用了”的结论。

形式化验证只检查：在既定定义、公理和已导入的基础库下，这段代码是否能推出那个定理。它不自动回答下面的问题：

● 这个问题是否值得研究？

● 这个定理的表述是否抓住了真正重要的现象？

● 前提是否恰当？

● 证明对应的人类论文是否准确传达了思想？

● 这个成果会对其他领域产生什么影响？

而且，形式化过程本身也有成本：把一份自然语言证明翻译成机器可检查的证明，需要补足大量被人类省略的细节。OpenAI 自己也明确表示，人类研究人员协助整理论文、将证明形式化，并对正确性负责；但数学论证本身由系统生成。

因此，更合理的角色分工不是“ AI 代替数学家”，而是：

AI 负责高速探索大量可能性；形式化系统负责卡住逻辑错误；人类负责选择问题、理解意义、审查边界，并决定下一步往哪里走。

对普通人来说，这意味着什么？

最先变化的未必是“ AI 明天解决所有未解难题”，而是研究工作的节奏。

过去，一位研究者可能花数月排除错误思路、补全技术细节、核对长证明。未来，AI 可以在这些环节承担更多探索和检查工作。研究者的时间会更集中在问题选择、概念判断和跨领域连接上。

这也解释了为什么数学突破值得关注：它展示的不是一个更强的答题机器人，而是一个逐渐成形的“研究闭环”——提出候选想法、发现错误、修正路线、生成论证、机器验证。

如果这种闭环能迁移到芯片设计、材料科学、药物研发或软件工程，前提是这些领域也能建立足够可靠的测试与验证机制，那么 AI 的价值就不再只是加快写作和编程，而是加快人类发现新东西的速度。

真正的门槛，不是 AI 会不会说“我找到了答案”，而是它能不能让答案经得起检验。

[attach]171622[/attach]

AICG 果园

欢迎光临数学中国 (http://www.mathchina.com/bbs/)