下载客户端

《AI与数学莱顿宣言》前史（一）：《在AI时代塑造数学的未来》

2026-06-05 17:05

来源：澎湃新闻·澎湃号·湃客

听全文

6月2日《AI与数学莱顿宣言》初版正式发布之后，陶哲轩做了积极评价（详见本文引言），除呼吁同行研读和酌情签署（截至北京时间2026.6.4，已有1300+人签署）之外，同时强调参与公共议题讨论的重要性，并推荐大家参阅前期（今年3月份）莱顿宣言初稿。

译者申明：感谢各位公众号读者留言建议，译文（尤其长篇）仅供参考，一切以原文原意为准（在很可能出现争议之处，我会尽可能引用原始内容供对比阅读，原文参考链接会始终在底部完整提供，如有个人或平台转载，请不要删除原作者提供的原始文献链接）

2025年9月在荷兰莱顿大学洛伦兹中心举办的研讨会

前排中间两位为参与莱顿宣言撰写的工作组成员：

Rodrigo Ochigame、Mateja Jamnik

图源：universiteitleiden.nl

作者：

约翰・科姆兰（Johan Commelin，荷兰乌得勒支大学助理教授，Mathlib Initiative项目负责人，Lean定理证明器数学库Mathlib维护者之一）

马特亚·亚姆尼克（Mateja Jamnik，剑桥大学计算机科学系教授 *）

Rodrigo Ochigame（莱顿大学助理教授，人类学家和历史学家 *）

兰尼·塔尔曼（Lenny Taelman，阿姆斯特丹大学代数几何教授）

阿克沙伊·文卡泰什 (Akshay Venkatesh，IAS普林斯顿高等研究院教授，菲尔兹奖得主) 2026-5-8

上述标*作者为莱顿宣言工作组成员。

译者：zzllrr小乐（数学科普公众号）2026-6-5

求点赞

求分享

求喜欢

引言

作者：陶哲轩 mathstodon.xyz/@tao

日期：2026.6.2

mathstodon.xyz/@tao/116681024360293007

最终文稿经过过去数月的反复打磨完善，成品令我印象深刻，我对此完全赞同、鼎力支持。宣言中的诸多观点在其他文献中也曾被提及，比如我本人的写作与谈话就多次探讨过其中部分内容，但把所有主张系统凝练在一份文件里，便产生了极高的额外价值。我呼吁业内所有同行研读这份宣言，并酌情签署（我本人已签署完毕 https://leidendeclaration.ai/signatories?q=Terence+Tao ）。

宣言里各项建议都十分中肯，在此我着重强调参与公共议题讨论这一条。现实中一个普遍问题是：一线数学家往往埋头钻研解题等技术性工作，疏于向大众阐释研究的内在意义。

So long as we had a near-monopoly on the ability to accomplish these tasks, we could have this luxury of only discussing "safe" technical topics in public; but in the new era of "proof abundance", it is increasingly important that we also debate the "soft" aspects of our field, such as our goals and values.

过去，攻克高深数学问题的能力近乎由数学家群体垄断，我们尚能只在公开场合谈论“稳妥”的纯技术内容；但在“证明唾手可得”的全新时代，学界必须主动探讨学科“软”性议题，例如科研目标与价值取向，这件事变得愈发关键。

另可参阅科姆兰（Commelin）等人今年3月发布于 arXiv 的莱顿宣言（文献链接：https://arxiv.org/abs/2603.24914 ）

在AI时代塑造数学的未来

作者：约翰・科姆兰（Johan Commelin）、玛泰娅・亚姆尼克（Mateja Jamnik）、罗德里戈・奥奇加梅（Rodrigo Ochigame）、伦尼・泰尔曼（Lenny Taelman）、阿克沙伊・文卡特什（Akshay Venkatesh）

日期：2026.5.8（第2版）2026.3.26（第1版）

人工智能正以前所未有的速度与规模重塑数学学科，倒逼学界重新审视这门学科赖以立足的知识根基。依托 20 世纪关于可计算性与数学基础的理论探索，当代人工智能早已跳出数值运算与穷举核验的范畴，发展出成熟的数学推演能力。AI 相关能力的飞速落地，催生了大量亟待整个数学界共同解决的新问题。

这场变革依托多元化、技术路线各不相同的人工智能方案全面铺开：越来越多数学家开始使用Lean 证明助手 ¹（基于传统符号逻辑的形式化验证系统），在协作式数学形式化项目中完成复杂定理的编码与证明核验 [1]。深度神经网络 + 符号结合的系统（如 AlphaProof）已达到IMO国际数学奥赛奖牌级解题水准；纯大语言模型类人工智能，也逐步转型成为数学科研辅助工具 [7]。尽管上述技术在实现路径与底层理念上存在显著差异，但它们共同具备改写数学知识发现、验证与体系化方式的潜力。

图源：荷兰莱顿大学

本文五位作者于2025年9月在荷兰莱顿洛伦茨科学中心主办了一场题为《机械化与数学研究》的专题研讨会 ²，汇聚数学家、计算机科学家、科学哲学家与科学史家，跳出短期技术细节，从宏观视角研讨 AI 带来的深层变革。会议研讨氛围热烈，所有参会学者都意识到这场变革事关数学的长远走向。本文立足作者参会心得，提炼关键结论，旨在推动数学界开展必要讨论：既不盲目神化现有科研范式，也不默认技术革新天然具备正向价值。

术语释义

形式化证明（formal proofs）

可由 Lean、Rocq、Isabelle 等机器系统自动核验的数学证明；

形式化证明库（libraries of formal proofs）

经过机器核验的数学命题与证明共享知识库，典型项目为 Mathlib、AFP（Archive of Formal Proofs）形式化证明档案库 ³。

人工智能（AI）

囊括符号派（symbolic）与神经网络（neural）两大技术路线，大语言模型亦在定义范畴内；各类工具实现路径不同，但均可助力数学推理自动化与新结论发掘。

数学共同体（mathematical community）

定义宽泛，包含高校与产业界科研人员、在读学生、独立数学贡献者。

下文围绕研讨会凝练出五大核心议题：数学的内在价值、科研实操范式、数学教育、前沿技术落地、智能系统衍生的伦理治理，逐一梳理关键问题与学界落地建议。AI 时代的数学未来绝非被动降临，而应由全球数学共同体携手共同塑造。

一、数学的内在价值

本次研讨会上各方观点分歧鲜明：一部分研究者欢欣鼓舞，期待计算机接管繁琐的证明撰写工作；另一部分学者则认为，推导与书写证明的过程本身就是数学技艺不可或缺的组成部分。有人主张形式化证明全面融入科研与教学，也有学者坚决反对该导向。种种分歧，折射出数学界宣称的价值理念与现实科研实践之间持续存在的内在矛盾。

这种广谱性反映了基础价值观的多元性，数学的价值根植于兼具人文属性与科学属性的独特学科传承，因此切勿用单一标签概括全体数学家的价值取向。

但当下的时代要求我们全面、审慎地审视数学价值的复杂内涵。手段会反过来重塑目的（Means reshape ends）：新技术的强大能力，有可能主导何为重要的数学研究，而非服务于数学本身的核心诉求。数学证明片段的自动化，会改变研究者的选题方向与受推崇的证明范式；依托形式化与机器验证提升严谨度，也将改写论文发表的评判标准。

And while some parts of the community may benefit from the increased commercial interest in mathematical AI, we must remain conscious of how such interest can reorient the field’s internal compass. Otherwise, our discipline risks losing its intellectual autonomy.

尽管部分学者能从资本对数学人工智能的追捧中获益，但我们必须警惕商业导向扭曲学科内在发展方向，否则数学或将丧失学术自主性。

上述问题由来已久，只因近年技术迭代的规模与速度，使其迫在眉睫。解决方案并无捷径，但研讨会达成一条广泛共识：

Ensure that the development and adoption of new technologies in mathematics remain firmly rooted in our own epistemic and aesthetic values—diverse as they are—rather than driven by the internal logic of those technologies or the commercial interests of their developers.

数学新技术的研发与落地，必须牢牢立足数学多元的认知与审美价值，不能受制于技术自身逻辑或研发方的商业利益。

各国数学学会、高校数学系与科研工作者，都应积极参与相关研讨，携手规划学科的发展道路。

二、数学科研范式的未来走向

现阶段我们尚无法预判：AI 系统能否、何时、在何种程度上超越人类完成标准化数学任务（例如生成完整形式化证明）。但洛伦茨中心的研讨结论明确：学界必须即刻直面该假设落地后的连锁影响。

整个共同体需要共同思考：一旦 AI 可批量生成形式证明，何谓数学新发现？是产出一份机器可验证的形式证明、提出关键性猜想、构建具备解释力的论证，还是其他成果？人类数学直觉的定位将如何变化？在科研模式剧变的环境下，我们该如何培养新一代数学家？据此提炼行动方向：

研究者应携手学生共同探讨：当机器承接当前数学研究大量日常工作后，人类与数学之间的关系将如何重塑。

三、数学教学与人才培养

如同手持计算器和旧时代技术普及带来的变革，人工智能将颠覆数学基础能力的定义，进而改写数学教育的本质目标。当计算机可以规模化完成标准化数学演算，人类数学素养的核心不再是手动演算，而是判断任务类型、厘清运算目的、串联具体问题与宏观研究方向，以及形成赋予数学意义的判断力与洞察力。

该变革同步带来考核难题：在 AI 可轻松完成常规计算与证明的环境下，如何通过考试测评学生真实的理解与能力？为提升数学共同体应对未来变局的韧性，学界建议：

修订本硕阶段数学培养方案，扩充教学能力边界，重点培养学生提出问题、学术交流、辨析逻辑论证优劣的综合素养.

教改研讨需吸纳学生参与，因为变革直接关乎他们的未来。

四、面向数学的人工智能技术建设

如何让数学家深度参与数学专用 AI 工具研发，掌握技术发展话语权？

形式化证明开源库已率先走出一条可行路径：成功吸纳海量职业与业余数学家共建。为保障这类知识库长期健康发展、贴合学术价值观，必须借鉴开源项目成败经验完善治理规则。

In particular, we must establish clear licensing frameworks and contributor norms that protect these libraries from unrestricted commercial use without attribution or respect for the rights of authors.

我们尤其必须制定清晰开源框架协议与贡献者规范，防范项目成果被商业主体无偿盗用、无视原作者著作权。

Another proposal being pursued by multiple groups is the creation of community-owned benchmarks. Good benchmarks can signal community values to those developing AI systems, while also helping mathematicians understand realistic use cases for, and limitations of, the technology. For example, benchmarks that focus on open-ended problems can counter overstated claims based on narrow task suites.

另一项学界共识方案：共建属于数学共同体的评测基准数据集。优质基准既能向 AI 研发方传递数学界价值导向，也帮助数学家认清 AI 真实能力边界与落地局限；聚焦开放性数学问题的基准库，还能遏制厂商基于窄域测试夸大 AI 性能的宣传乱象。

当前顶尖数学推理 AI 多由商业科技企业闭源研发，但开源、权重开放的同类模型正不断涌现（如 Goedel-Prover、Kimina-Prover）[5, 8]。闭源与开源路线既存在良性竞争，也可在学界内部、产学研之间协同互补：交叉验证、技术互补、经验互通，助力整个行业理性推进数学 AI 研发。

据此确立建设目标：

搭建学术导向的数学 AI 基础设施：代码开源、决策透明、由学界共同监督，降低数学领域对单一商业企业的技术依赖。

这套公共基建除守护数学学术独立外，还能实现算力成本、训练数据、能耗环保等关键信息公开透明，让技术研发始终对齐数学共同体的发展优先级。

五、行业规范、科研伦理与治理框架

人工智能融入数学研究，衍生出诸多突出的伦理与治理难题。

The training of such systems uses the work of the mathematical community in an opaque way that threatens established norms of attribution and credit. AI-generated papers are starting to put still more pressure on a publication system already strained to the breaking point; and how should formal proofs be integrated into this?

这类人工智能系统在训练过程中，以不透明的方式取用数学界前人的研究成果，动摇了现行的成果署名与学术确权规范。由人工智能生成的论文，进一步加重本就濒临承压极限的学术出版体系负担；而形式化证明又该如何纳入现有出版规则，目前尚无定论。

Mechanization may also create new forms of inequality, in which disparities in access to computational resources distort the competitive dynamics of mathematical research. Moreover, the substantial energy demands of AI systems raise important environmental concerns.

机械化工具还可能催生新的科研不公：算力资源获取条件的差距，会打破数学科研公平竞争的格局。除此之外，人工智能模型庞大的能耗需求，也带来不容忽视的环保问题。

为此学界提出落地建议：

Develop and maintain a living statement of ethical principles to guide academic mathematicians and mathematical institutions in their interactions with AI systems and developers.

编制并动态更新数学 AI 伦理准则规范，指导数学研究者与科研机构规范和 AI 技术方的合作。

该伦理文件不具备强制法律效力，也无法穷尽全部细则，经由广泛学界磋商形成，凝练全行业共识与行为规范（对标 1975 年重组 DNA 阿西洛马伦理会议模式[6]），内容涵盖：成果署名与引用规范、算力与训练数据披露要求、预印本与形式证明库开源授权细则、AI 使用行为守则。文件需由各国数学学会牵头常态化修订，持续适配新兴技术挑战；本次研讨会已有参会学者启动准则起草工作。

结语：主动参与 AI 与数学的议题共建

层出不穷的 AI 新闻，容易让一部分研究者心生质疑，也会让另一部分人被动躺平、消极认命。本文呼吁所有读者主动投身相关讨论：学习 AI 技术原理与能力边界，和同事、学生、行业学会深入交流，立足自身科研体悟梳理个人数学价值观，并落地集体行动。

当下正处在数学发展的关键十字路口，学科的未来定义权正在重新博弈。积极参与相关研讨，就是让数学的未来扎根全人类数学家共同的理想与价值。

原文参考文献

[1] J. Commelin and A. Topaz (2024)：纯数学中的抽象边界与规范驱动开发，《美国数学会通报》第 61 卷第 2 期，241–255 页

https://dx.doi.org/10.1090/bull/1831

[2] Lean 社区 (2020)：Lean 数学库，《ACM 第 9 届认证程序与证明国际会议论文集》，367–381 页

https://dx.doi.org/10.1145/3372885.3373824

[3] L. de Moura 等人 (2015)：Lean 定理证明器（系统综述），CADE 第 25 届自动推理会议，《计算机讲义》9195 卷，378–388 页

https://dx.doi.org/10.1007/978-3-319-21401-6%5F26

[4] T. Hubert 等人 (2025)：《基于强化学习实现奥赛级形式数学推理》，《自然》651 卷 (8106)，607–613 页

https://dx.doi.org/10.1038/s41586-025-09833-y