LLM框架用于发现重大数学猜想：AI探索下一个黎曼猜想

重大数学猜想的提出，长期以来被视为数学智慧的最高体现之一。无论是黎曼猜想、哥德巴赫猜想，还是千禧年难题，它们的诞生往往来自少数数学家在长期思考中的灵光一现或深刻洞见。这种对专家直觉的严重依赖，使得猜想发现难以被系统化地复制、评估和验证。arXiv 上最新发布的一篇论文尝试改变这一现状：研究人员提出了一套以大语言模型（LLM）为核心的三阶段流水线，用于自动生成并验证具有实质数学潜力的猜想，目标被明确称为“下一个黎曼猜想”级别的探索。

这套流水线的第一阶段是区域搜索（region search）。与之前一些从零开始随机生成命题的做法不同，该阶段要求模型从显式的局部证据模块出发。所谓局部证据，可以理解为一些在特定数学领域中已经被验证为真、或具有较强支持的小范围事实。模型在这些证据的引导下，在某个数学子领域中搜索可能成立的候选猜想，从而避免完全盲目的生成。第二阶段是反思性验证（reflective validation）。系统会从基础性（foundationality）、新颖性（novelty）和潜在重要性（potential significance）三个维度对每个候选进行内部批判。基础性考察候选命题是否扎根于核心数学结构，新颖性考察它是否区别于已有结果，潜在重要性则衡量一旦被证明，它对理论发展的推动作用。第三阶段是形式化验证（formal validation）。候选猜想会被交给 Lean 4 证明助手及其数学库 Mathlib，用机器可检查的严格逻辑语言重新表述。只有通过了 Lean 的解析与类型检查，候选猜想才算在形式上获得了合格证。

研究者用一个颇具感染力的概念概括这项工作的目的——“问题品味”（problem taste）。一个有高度问题品味的数学问题，其证明有可能重新组织一个研究领域的语言，为后续大量工作提供新的框架和工具，并对人类数学研究提供持久的帮助。换句话说，这项研究不只是想生成一堆“可能正确但无关紧要”的命题，而是希望找到那些一旦被证实就能改变领域走向的核心问题。

论文报告了二十个候选猜想的实验结果。数据显示，从自然语言表述到形式化检查的过渡相当稳定：二十个候选全部通过了 Lean 4 的解析和类型检查；全部二十个都没有被 exact? 这一自动化策略直接吸收；也全部都没有被 aesop 这类自动证明搜索工具直接消解。此外，系统没有发现这些候选之间存在显式重复或近似重复。尽管这只是一次规模的演练，但作者认为，这表明流水线有能力在保持一定质量门槛的同时产出多样化的候选猜想。

该论文由 Alizer Wong 与其他七位作者共同完成，全文二十五页，包含一幅图，于 2026 年 4 月 19 日提交至 arXiv，编号为 arXiv:2607.28632 [cs.AI]，并配有 DataCite 生成的 DOI（https://doi.org/10.48550/arXiv.2607.28632）。投稿历史显示，第一版（v1）由 Zixin Zeng 提交，文件大小约 1,319 KB。论文并未声称已经发现了真正的“下一个黎曼猜想”，而是提出了一套可复现的方法论，让 AI 能够以更严格、更透明的方式参与数学发现。对于关注 AI for Math 的研究者和工程师而言，这项工作展示了大语言模型与形式化验证工具结合的一种新范式，也提醒我们：未来数学中的创造性工作，可能会越来越多地由人类与 AI 共同完成。