事件概述

2026 年 8 月，一篇来自 arXiv 的论文提出了一个基于大语言模型（LLM）的框架，用于系统性地发现重大数学猜想，目标直指“下一个黎曼猜想”。该论文由 Alizer Wong、Zixin Zeng 等八位作者共同完成，于 2026 年 4 月 19 日提交，归类于计算机科学的人工智能子领域（cs.AI）。

论文指出，当前重大数学猜想的提出仍然高度依赖专家直觉，缺少一种统一的方法来系统生成和验证具有实质数学潜力的猜想。为此，作者设计了一个三阶段流水线，将自然语言表述的候选猜想逐步转化为经过形式化验证的数学命题，并在 20 个候选猜想上进行了实验验证。

关键技术点

该框架的核心是一个三阶段流水线：

  1. 区域搜索（Region Search）：从显式的局部证据模块出发，在数学空间中搜索可能存在有价值猜想的具体区域。这一阶段不直接生成完整猜想，而是利用局部证据缩小搜索范围，为后续生成提供候选“区域”。

  2. 反思性验证（Reflective Validation）：对搜索到的候选猜想进行多维度评估，包括：

    • 基础性（Foundationality）：该猜想是否扎根于数学的基础结构。
    • 新颖性（Novelty）：是否与已有结论不同，是否存在直接重复或近似重复。
    • 潜在重要性（Potential Significance）：该猜想如果被证明，是否可能重组一个研究领域的语言体系，并对人类数学研究产生持久帮助。

  3. 形式化验证（Formal Validation）：使用 Lean 4 和 Mathlib 对候选猜想进行机器可检查的验证，包括语法解析、类型检查以及自动证明尝试。

论文特别强调“问题品味”（problem taste）——即那些证明过程可能重构某个研究领域的叙述方式、并能长期帮助人类数学研究的问题，才是高价值的目标。

实验与结果

论文在 20 个候选猜想上进行了实验，结果如下：

  • 20/20 的候选通过 Lean 解析和类型检查；
  • 20/20 的候选未被 exact? 直接吸收（说明不是显然成立的已知定理直接变形）；
  • 20/20 的候选无法被 aesop 自动消解（说明具备一定的证明难度）；
  • 未发现显式重复或近似重复的猜想。

这说明了从自然语言到形式化检查之间存在“稳定通道”，候选猜想在形式化层面均有效且非平凡。

对数据科学或 AI Agent 落地的意义

这项工作对 AI 驱动的科学发现具有重要的示范意义。它展示了 LLM 不仅仅是文本生成工具，还可以被组织成“提出—评估—验证”的闭环 Agent 流程，用于解决高度创造性且需要严谨逻辑的数学研究任务。具体而言：

  • AI Agent 的可控性：三阶段流水线将开放式的猜想发现分解为可追踪、可验证的子任务，降低了 AI 生成内容的不可靠风险。
  • 形式化验证作为安全网：引入 Lean 4 等证明助手，为 AI 输出提供客观的“正确性”过滤器，这对于任何 AI 科学发现系统都是关键的信任机制。
  • 问题品味的概念化：“问题品味”被转化为可操作的标准（基础性、新颖性、潜在意义），使得 AI Agent 能够根据高层次科研价值观进行选择，而不仅仅是追求局部最优。
  • 对数据科学方法论的启发：数学猜想发现与数据科学中的假设生成有相似之处——从数据（局部证据）出发，生成候选假设，筛选并验证。该框架的“搜索—反思—形式化”三层结构可迁移到更广泛的科学假设发现系统中。

我的技术点评

这是一个非常有野心的方向，但我也保持审慎。论文的亮点在于将“数学品味”这种抽象能力工程化为可执行的管道，并用 Lean 4 作为最终裁判，这比单纯用 LLM 生成猜想再人工筛选要严谨得多。

不过，从结果来看，20/20 通过形式化检查本身并不等同于这些猜想是“重要”的。exact? 和 aesop 无法自动证明只说明候选不是显然的简单结论，但距离“重大数学猜想”仍有巨大距离。论文中未给出这 20 个候选猜想的实际内容示例，也未说明它们是否已被证明或证伪，这让我难以判断其真正价值。

另一个值得注意的点是，论文标题提到“下一个黎曼猜想”，但摘要和正文均未提供任何与黎曼猜想直接相关的具体进展。官方原文也未说明这些候选猜想是否属于数论领域，更未提及是否与黎曼猜想有关。因此，标题带有一定的修辞色彩，实际贡献更多在于“框架”，而非具体猜想本身。

此外，论文的作者列表中并未给出机构信息（原文未说明），因此无法判断其背景。这并不影响技术内容，但在评估研究可信度时是一个缺失信息。

总体而言，这篇论文为 AI 参与纯数学前沿研究提供了一个可复现的范式。未来的工作如果能在实际数学家中引起共鸣，并产生哪怕一个被证明有意义的猜想，就将证明这条路线真正可行。我期待看到后续工作公开更多候选猜想的细节和实际评估结果。

原文链接