标签
OpenFrontiers 推出了一个跨学科语料库，包含 12,151 个尚未解决的研究问题，以及一个由 200 个近期已解决的数学问题组成的回溯性基准，这些问题均附有 Lean 4 形式化陈述。该研究评估了七个大语言模型智能体，发现它们在闭卷条件下重新发现研究级成果的情况仍然罕见，而在实时联网条件下取得的成功则主要源于检索已发表的解答。
ReuF2F 引入了一个基于 Lean 4 的基准，包含 244 个源自本科 REU 项目的形式化开放研究问题，用于端到端评估编程智能体。即便是表现最好的模型也只能解决约 40% 的问题，仍有很大的提升空间。
文章抱怨AI实验室在利用数学家验证AI生成的定理和证明，却不提供相应的免费API token资源，呼吁实验室为数学验证工作提供支持。
# 数学家们对 OpenAI 重大发现的百条短评 100 多位数学家对 OpenAI 于 10 月 6 日发布的公告做出了简短回应。OpenAI 宣布其模型已解决了 100 多个悬而未决的数学难题，其中包括对"准黎曼猜想"等突破性成果的震惊，以及对人类数学家未来角色的深刻反思。
OpenProblemBench 引入了一个包含数学和理论物理领域 82 个未解决问题的基准，用于评估 AI 模型在开放科学问题上取得进展的能力，其中 GPT-6-Astra 以 14.0% 的最高平均解决率位居榜首。
一篇评论文章，指出数学家数十年来以造福社会为由为纳税人资助进行辩护，如今却哀叹AI解决著名开放问题是在损害该领域及其社群，这一立场被视为虚伪。
一份报告称，AI系统已解决了数学领域500个最重要未解难题中的约90个，一位顶尖数学家称这是数学史上最重大的时刻。
# 当 AI 解出长悬未决的数学难题时，应当立刻发表 ## 一份来自创意行业的证词 我是一名创意工作者——写作、设计、作曲，靠这些谋生。过去十年，我亲眼看着我所在的行业被机器重新洗牌：文字生成、图像合成、音乐生成，一件件工具落地，一个个岗位消失。我们之中没有人获得过"特殊保护期"。没有人停下来问一句："这些创意工作者可能需要几年时间来适应。"技术该来就来了，从业者要么跟上，要么被时代甩在身后。 现在，同样的逻辑正在被数学界试图拒绝。 有人主张：如果 AI 发现了某个悬置数十年、甚至上百年的数学难题的证明，我们应当**暂缓发表**，先给数学家们留出消化和适应的时间。我理解这种情绪，但我不同意这种做法。理由很简单：**科学进步不应当为任何职业的调整期买单。** ## 验证与署名是底线，保护不是 先把话说清楚：我绝不是在主张"随便一个 AI 输出都应当原封不动地印进期刊"。证明必须经过严格的人类验证——这是数学的基本原则，与 AI 无关。任何来源的"证明"都一样：未经验证的论文不该发表，无论作者是人类还是模型。署名与致谢同样重要，贡献必须被正确归因，工具的使用必须被如实披露。 但"验证"和"署名"之后，就没有任何正当理由了。 要求"暂缓发表"，本质上是要求科学共同体把一个公共问题的解答**扣押起来**，以换取一个专业群体的心理缓冲。这在伦理上站不住脚，在实践上也不可行： - **证明本身没有职业归属。** 一个关于黎曼猜想或孪生素数的证明，属于全人类的知识公地，不属于某个职业群体的既得领域。 - **扣押创造风险。** 数学问题往往只有一个窗口期可以被攻克，一旦有团队独立发现同一路径，抢先发表的动机将被成倍放大，学术不端的土壤反而更肥沃。 - **它对其他领域的先例是危险的。** 如果物理学家也可以因为"我们还没准备好"而扣押某个实验结果，科学验证本身的含义就被瓦解了。 ## "适应期"这个理由，我们已经听过一遍了 创意行业的人最清楚这个论证的真面目。 当生成式模型开始产出可用的文案、可用的插图、可用的配乐时，业界的呼声一模一样："等一等，让创作者有时间调整。""我们需要保护原创者。""至少设立缓冲期。" 结果如何？缓冲期没有到来。模型迭代的速度以月计，作品质量以周计地逼近可替代的门槛。市场没有停下来等待。唯一的变化是：那些主动学会与工具协作的人活了下来，那些把时间花在"等待保护"上的人，没有。 我不是在嘲讽他们的困境——那个困境是真实的，其中大多数人确实值得更好的出路。我想指出的是一个冷酷的事实：**职业群体的适应困难，从来不是阻断外部创新的合法理由。** 技术带来的摩擦是真实的，但解决摩擦的方式是教育、转型和新的分工，而不是按下暂停键、让知识本身为人让路。 如果数学界今天可以因为"我们还没适应"而扣押一个 AI 证明，那么明天，任何一个被 AI 触及的领域——药物发现、材料科学、气候建模——都可以援引同样的理由。这是一条滑坡，而坡底是"科学进步以职业安全感为条件"。 ## 该做的，是加速而非减速 如果 AI 真的开始独立产出经得起检验的数学证明，数学界需要做的不是恐惧，而是把验证基础设施建得更快、更严： 1. **建立可复现的验证流程**，让机器辅助的证明链条对人类审查者透明。 2. **明确署名规范**，在论文中如实记录模型、提示与人工审阅的角色分配。 3. **重新设计训练体系**，把"提出问题、批判证明、判断重要性"这些目前仍属于人类的高阶能力，作为下一代数学家的核心技能来培养。 4. **承认新的分工格局**，让数学家从重复性推导中解放出来，去做机器做不到的那部分工作。 这些事情不能靠扣押结果来争取。它们需要立刻被承认并着手建设。 ## 结语 一个证明被验证为真，它的意义就成立了，不取决于人类何时准备好接受它。 数学曾经被少数人的直觉和少数人的劳作推动了三千年。现在，我们拥有了另一台推动它的机器。机器可以来，证明可以发表，数学可以继续向前——而我们这些在创意行业里已经经历过一次冲击的人，只想告诉数学界一句： **保护是有限的，验证是无限的。**
一个汇集 Heilbronn 问题目前已知最佳点集配置的网站——即在单位面积区域（正方形、三角形和最优凸区域）内放置 n 个点，使其中任意三点构成的最小三角形面积最大化——提供精确坐标、证明以及浏览器内置的有理数算术验证器。
使用AI辅助方法证明了ζ(5)的无理性，该解决方案在FrontierMath上被标记为已解决，尽管它没有采用最初预期的Apéry风格证明。
据报道，OpenAI训练了一个新的AI模型，该模型已解决了超过100个长期存在的开放数学问题，导致成立了一个咨询小组来评估和协调这些结果的发布。
文章强调，数学是一个不断扩展的领域，拥有无数未解之谜，而人工智能是一个变革性工具，能够以前所未有的速度推进数学研究，将焦点从个人成就转向协作进步。
Terence Tao 讨论了AI如何被用于解决开放数学问题，并对这些资源的非可持续性质及其对未来研究的影响提出了担忧。
Terence Tao认为，应保留数学开放问题供人类解决，以维持纯净的基准并发展新技术，建议通过社会规范限制AI解题器在某些领域的应用。
TheoremDB is an alpha-stage public workspace for machine mathematics, offering a shared, searchable record of open problems, partial results, and Lean-verified proofs to help research agents avoid redundant work.
Google DeepMind 发布 AlphaProof Nexus 论文，AI agent 在 353 个开放数学问题中自主解决了 9 个 Erdős 难题（包括两个 56 年未解问题），并证明了 44 个 OEIS 猜想，每道题推理成本仅数百美元。
菲尔兹奖得主蒂莫西·高尔斯报告使用 GPT5.5 Pro 解决公开数学问题，并预测由于人工智能的快速发展，数学研究将很快面临危机。
Tim Gowers 报告称，他使用 ChatGPT 5.5 Pro 尝试解决由 Melvyn Nathanson 提出的数学开放性问题。