Mathematics in the age of AI
如果AI最终能解出研究级数学证明,数学界真正该守住的是什么
这篇文章基于作者在2026年国际数学家大会上的演讲,没有纠结于AI现在到底能不能做研究级数学,而是直接假设这种能力迟早会出现。在此前提下,文章追问数学共同体实际在追求和优化的目标究竟是什么,并以解题这项工作为案例展开分析。作者指出,光是得到正确答案远远不够,理解、表达和社群认可同样重要。
他们做了什么
- 作者提出一个工作假设:AI迟早能够胜任相当一部分研究级数学任务,并在此假设下探讨数学界需要重新审视哪些一直未曾明说的价值观。
- 以解题为例,目标被逐步细化:从最初的尽可能多解开难题,依次加入正确性验证、清晰表达、被社群消化接受、最终融入该领域的权威理论体系,共五个阶段。
- 文章警告,AI生成的证明即便通过形式化验证也可能无人真正理解,或者被打磨得过于流畅,以至于真正困难的步骤和常规步骤看起来一样简单,读者失去了辨别重点的线索。
- 作为实证,First Proof项目第二批测试中,四个AI系统面对十道从未在网上公开过的全新研究级问题,其中七道题至少有一个系统获得专家评审的及格评价,每题计算成本大约在几十到几百美元之间。
- 文章引用了2026年6月发布、获国际数学联盟支持的《莱顿人工智能与数学宣言》中的若干建议,包括披露AI工具使用情况、方便同行评审、坚持人类作者身份、努力做好来源归属等。
![Figure 3. A page from a 1991 paper of Bourgain [3], annotated by my much younger (and very frustrated) self. But by fighting my way through these texts, I came to understand Bourgain’s way of thinking, and in time I actively sought out his papers to read. See also [19], [17].](https://media.metallab.ai/papers/2608.16753/f0.jpg)
为什么重要
一旦AI生成证明的速度超过学界验证、撰写、评审和归纳整理的能力,原本为证明稀缺时代设计的期刊、评审、晋升等制度可能在证明过剩的时代运转失灵。这篇文章提醒所有关心知识如何被生产和信任的人:又快又对的答案,不等于被理解、被信任的知识。
本文术语
- 古德哈特定律(Goodhart's law) · 一旦某个衡量指标变成追求目标,它就不再是好的衡量指标
- 自动形式化(autoformalization) · 把人写的数学证明自动转换成Lean等可由计算机验证的语言
- 经典化(canonicalization) · 把已证明的结果整理成最自然的表述形式,并纳入教科书和标准知识体系的缓慢过程
- First Proof项目 · 用从未公开发表过的全新研究级问题来独立评估AI数学能力的项目
- 莱顿宣言(Leiden Declaration) · 2026年6月发布、获国际数学联盟支持的关于人工智能与数学的23条建议
论文原文摘要（英文）
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website. Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them. Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
在 arXiv 阅读最新论文
- Improving Natural-Language Combinatorial-Optimization Accuracy in Resource-Constrained Language Models via Formal Abstractions给小模型一门专用的排程小语言,就能让它写出真正可行的日程安排
- SESSE: Sketch, Expand, Sort, Summarize, Evaluate -- LLM-as-Judge Evaluation via Structured Decomposition让AI裁判在挑选两个回答哪个更好时,把判断依据一条条摆出来
- Position: AI Leaderboards Are Underserving the Global South: A Case Study from India印度等全球南方地区其实已经有优质AI基准测试,缺的是能公正排名的独立裁判机构
- Temporal Multi-Signal Fusion for Token-Level Hallucination Detection识别AI编造的内容,不能只看单个词,要看上下文的连续变化
- Evaluating Structured Information Extraction with Open Models in a High Risk Public Sector Application在高风险公共部门文档任务中,开源AI开箱即用有四分之三不合格
- When Clean Signals Are Not Enough: Detecting Structural Ambiguity for Safe Wearable Stress Classification一款平均准确率93%的压力检测AI对某一个人完全失效,研究者因此做了一个在分类前先检查信号是否可信的把关系统
- Bridging Search and CRM: Productionizing AI Product Research Agents for Customer Re-EngagementAI智能体追着离场用户发WhatsApp,把逛而不买的顾客拉回来
- Pairwise Ranking Outperforms Single-Action RL for Offline Explanation Selection: A Practical Lesson推荐理由不必每次现写:提前生成一批候选,再挑一个就够好
METAL LAB 最新报道
图片来源： jonbaer et al., arXiv:2608.16753, arxiv-nonexclusive