AI会杀死研究论文吗？数学家给出新答案

论文制度的压力早已存在，AI只是加速器

在Lex Fridman的播客中，数学家们抛出了一个听起来近乎荒谬的问题：AI会杀死研究论文吗？但讨论很快转向一个更现实的观察——学术期刊体系在AI大规模介入之前，就已经承受着巨大压力。

据节目中的观点，数学期刊长期面临投稿量激增与审稿人疲惫的双重困境。审稿人需要花费大量精力去理解并验证定理，而越来越多人产出知识的速度远超审稿系统能消化的速度。一位嘉宾直言：“唯一比这个系统更糟的，是没有这个系统。”因为数学的认识论——我们如何抵达真理——本质上要求缓慢、谨慎和精确。

这种压力并非AI造成，但AI生成的论文和证明正在让审稿任务雪上加霜。节目中有人提到：“现在我们要面对的任务是，总得有人去审所有这些AI生成的论文。”

从论文到可复用组件：工程领域的启示

讨论中一个关键分歧在于“学术贡献”的定义。在工程和应用科学领域，贡献的形态早已多元化。写一段可复用的代码、维护一个数据集、提供一个API，这些都可能比一篇15页的PDF更有价值。尤其在大型协作项目中——比如LIGO或需要数百人参与的癌症研究——成果从来不是单一论文，而是代码、数据和可复用模块的集合。

嘉宾认为，AI时代会让这种趋势更加明显：一个能被社区或AI直接调用的小组件、代码库或数据集，其价值可能超过单个结果或单篇论文。这给纯数学领域带来了一个值得思考的问题：数学的“可复用性”该如何体现？

Lean与Mathlib：数学的形式化革命

节目中重点介绍了Lean和Mathlib。Lean是一个交互式定理证明器，最初为写出无bug的代码而设计。它的工作方式是逐行检查证明，计算机判断每一行是否从上一行的目标状态通过逻辑推理得出。Mathlib则是Lean生态中用于形式化数学的大型通用库，维护良好、组织严密，让研究者不必从皮亚诺公理开始定义自然数。

嘉宾指出，Lean和Mathlib正在改变数学论文的写作逻辑。传统数学论文存在一个根本问题：没有完美写出的定理规范。随便翻开一本数学书的一页引理，背后有大量上下文被省略，作者默认你读过前面60页。这导致数学结果无法像火箭的物理零件那样“开箱即用”。

而如果数学在未来全部形式化，规范就内建于对象之中——Lean不会让你错误地使用一个定理。这正是Mathlib十年前的梦想：让数学像科学一样运行。

交互式定理证明器（Interactive Theorem Prover, ITP）是一类软件工具，用户在其中输入数学定义与证明步骤，系统实时检查每一步是否逻辑有效。与自动定理证明器不同，ITP 强调人机协作：人提供证明思路和关键引理，机器负责验证细节并防止错误。Lean 是其中较新且活跃的代表，它依赖依赖类型论（Dependent Type Theory）作为基础，使得数学对象和命题都可以统一表示为类型，而证明就是构造该类型的项。这种“证明即程序”的对应关系（Curry-Howard 同构）让 Lean 既能验证数学证明，也能用于编写高可靠性软件。Mathlib 则是在 Lean 之上构建的数学知识库，目前已包含从基础代数到前沿研究的大量形式化内容，其组织方式类似软件库，支持导入、复用和自动化检查。

GitHub模式与开源社区的疲惫

讨论还延伸到了开源社区。GitHub上代码的爆炸式增长让维护者不堪重负，大量pull request让少数核心维护者心理和精力上都难以承受。这种疲惫与学术审稿人的困境高度相似：两者都依赖人类的动机和热情，一旦被耗尽，系统就会出问题。

Mathlib的运作模式被拿来作为对照：不是论文，而是pull request。维护者和审稿人会在PR中提出建议，整个过程公开可见——谁贡献了哪个想法、哪个简化、哪里可以复用已有引理。这种透明度是传统期刊审稿无法提供的。

Pull Request（PR）是 GitHub 等平台上的协作机制：贡献者提出代码修改请求，维护者审查、讨论并决定是否合并。这种模式将变更透明化，允许任何人评论和追溯。然而，随着开源项目规模扩大，PR 数量激增，核心维护者需要投入大量时间进行代码审查、回复讨论和解决冲突。研究显示，许多关键开源项目仅靠少数志愿者支撑，长期过载导致维护者倦怠甚至项目停滞。这与学术审稿人面对海量投稿的困境高度相似：两者都依赖有限的人类注意力和内在动机，缺乏可持续的激励与分工机制。

AI证明需要新的验证模式

对于AI生成的数学证明，嘉宾持谨慎但开放的态度。自然语言证明不可信，因为这些系统是随机过程，它们说出的话不代表它们真的“理解”数学。但自动形式化已经发展到可以让AI写出Lean代码，在Mathlib基础上逐层检查到公理层面。

节目中提到OpenAI在快速傅里叶变换上的改进成果，以及Twitter上人们接力改进常数的现象。嘉宾表示自己不在Twitter上，不太确定该如何看待这些碎片化的进展，但认为需要新的模式来组织和整理这些改进，而不是简单地套用旧有的论文体系。

有人提议，或许可以借鉴Mathlib的众包模式，让社区协作验证AI证明，同时保留传统期刊的严谨性。这不是要取代旧系统，而是缓解它已经承受不了的压力。

论文不会消失，但形态会变

综合多位数学家的观点，论文作为一种知识载体不会突然死亡，但它不再是唯一甚至不一定是最重要的贡献形式。形式化工具让技术细节可以被机器验证，研究者可以把更多精力放在思想的传播和解释上。

一位嘉宾提到，自己最喜欢做研究演讲的原因是可以把论文中杂乱的复杂度剥离，突出那个真正激动人心的核心想法和特例。当Lean接管了技术验证，写作本身或许能回归到更本质的东西：讲清楚为什么这个想法重要。

数学的独立性文化也是一个变量。数学家群体普遍不喜欢被指挥、偏好孤独工作，这与大型协作项目要求的集体组织模式存在张力。如何在保持个体创造力的同时建立新的协作验证机制，是AI时代数学界需要回答的问题。