下载客户端

一位Mathlib维护者的心声《形式化：数学理解的具象载体》by 菲利波・A・E・努奇奥（Filippo A. E. Nuccio）2026-10-15

2026-11-09 13:00

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

听全文

★置顶zzllrr小乐公众号，追踪《小乐数学科普》系列报道，参与数学 vs AI投票！

坚持不炒作的数学与AI报道，投稿信箱zzllrr@gmail.com

形式化：数学理解的具象载体

作者：菲利波・A・E・努奇奥（Filippo A. E. Nuccio）

法国圣埃蒂安大学副教授，Mathlib维护者之一（2026德马伊（Demailly）奖授予Lean开源社区MathLib项目）

日期：2026-11-8（收稿日期2026-10-15）

AI 使用情况：全文未使用人工智能。文末附有完整声明（“AI 声明与许可协议”）。

作者免责声明：

我是 Lean 主流形式化数学库 Mathlib（https://leanprover-community.github.io/index.html）的维护者之一，但下文所有观点仅代表我个人，绝不代表 Mathlib 社区及其治理团队的官方立场。

引言

当下数学界不断收到各大大模型给出的大量数学结论，围绕三件常常交织在一起的话题，相关讨论越来越多：一是“数学的本质在于理解”；二是这场变革受冲击最大的是博士生以及青年学者；三是 OpenAI、Anthropic 这类企业种种做法有失妥当。除上述批评之外，我们还频繁看到“形式化”一词，很多时候还会连带提到“Lean”。我认为这四条线索彼此关联，其关联方式或许出乎不少人的意料。

本文的核心主线：“理解数学”这个概念很美，但极难定义。我们到哪一步才算真正理解？理解究竟意味着什么？我们能不能把一份理解有条理地传递给同行，甚至传递给学生？能不能拿出一份凭证，证明理解已经发生？理解能不能产出可复现的成果？在多大程度上，数学理解本身是一种科研产出，而不只是一种思考方法？这种理解是否可以接受常规的科学检验？我们能不能核验它？

我的论点是：人工形式化数学，可以回答上面这些问题。做形式化工作，不仅能让我们理解得更深，还能产出科研成果，而这份成果承载的内容，恰恰就是这份理解。下文将顺着六年前我投身形式化的缘由展开，说明为什么这项美好的人类事业，核心在于理解数学，而非服务人工智能。

小段题外话：值得忧虑的往事

我们先暂停，回看前面提到的三点：数学重在理解、我们关心青年一代、科技企业的行为受纯粹经济目标驱动而失当。这让我想起另一场旷日持久的争论。

我长期支持开放获取（Open Access），也参与不少相关推广组织，包括 MathOA（https://www.mathoa.org）以及法国开放科学委员会（https://www.ouvrirlascience.fr/the-committee-for-open-science/）。在参与这些工作时，我常常提出：仅仅把爱思唯尔、施普林格、威立这“三大出版商”当成开放获取（无论数学还是其他学科）发展的主要阻碍，其实是转移焦点。

真正的症结在我们社群内部——也就是数学家群体：我们过分看重论文清单、期刊分区。是我们决定谁能拿到终身教职、提拔青年学者、评审和发放基金；而我们评判的依据，往往就是大家在（大多属于私人资本的）顶刊上发表的亮眼成果。

这套评价体系几乎不看重理解本身，反而逼迫青年学者乃至资深研究者，尽可能快、尽可能多地在顶刊发文章，才能让自己的工作获得认可。遗憾的是，长久以来，在我们的圈子里，博士生、博士后花时间沉下心去理解问题，其价值远比不上在爱思唯尔、施普林格、威立旗下期刊发论文。

我们选择了一条轻松的出路：宣称数学就是产出新结论，把问题全部归罪于这三家无良出版商，把他们视作元凶，却拒绝改变自身内部运行规则——而改变规则的主动权，本就在我们自己手中。

我反复听到大家呼吁：要缓解“不发表就淘汰”这套压在我们、尤其压在学生身上的压力，要收回大型出版商拿捏我们社群的权力。但过去十五年，局面几乎没有变化。如今每次 AI 证明出新定理，就有大量声音呼吁“重新思考我们的职业”，看到这些呼吁时，我不免担心历史重演。

但和出版业这个看似无解的困局不同，眼下我们有一条切实可行的路：接纳形式化，把它当成一门成熟的数学分支，它的使命就是梳理清楚“理解一条论证”究竟意味着什么。

通过形式化理解数学

为了说明这套梳理如何落地，我先讲一点我的疑虑：即便抛开“理解”这个词本身模糊不清的问题，“数学的本质就是理解”这个说法本身也站不住脚。数学不可能只有单一内核——两千五百多年来，数十万研究者投身其中，高尔斯9月17日的博文（数学家心声：蒂莫西·高尔斯“我为何没有签署菲尔兹奖得主的公开信”2026-9-17）已经把这点讲得非常透彻。同理，我不敢断言形式化数学真正的内在价值是什么；但我想说明，为什么我认为它是看待数学一个极好的视角：它更关注理解，而不是证明新定理。

这里不展开技术细节，只简单说明：在 Lean、Rocq、Isabelle、HOL-Light、Agda 这类证明助手中做数学形式化，就是用对应的语言写出定义、命题，再写出代码，代表命题的证明。绝大多数情况下，我们不能直接照搬论文、专著里那些非形式化的文字来完成。

所以更准确地说，形式化数学分为两步：首先反复思考该如何表述定义、命题和证明；其次把它们写下来。很多时候，我们处理的对象，是别处已经以某种形式存在的数学定义、已经存在的证明，只是它们原来的写法不适合形式化。

这种不适配可能体现为：泛化程度不合适、冗长计算掩盖核心思路、论证重复，导致我们提炼不出通用模式。既然产出全新数学结论并不是它的核心目标，这个方向长久以来都面临一个质疑：它到底算不算数学？

当年我和好友兼同事罗布·刘易斯一同创办《形式化数学学报》（AFM，https://afm.episciences.org），我们拟定期刊宗旨与范围，在编委会协助下定下审稿标准，其中两条写道：

数学形式化不是机械劳动：它本身就需要深刻的数学洞见，这正是形式化数学的内核；

证明审核（审计），也就是核验形式化命题能否准确对应非形式化的原始表述，是形式化论文审稿中难度很高、且本质上离不开人的环节。

在我看来，这两句话很好地概括了形式化数学的科学内核，也解释了为什么它是承载、探讨数学理解的绝佳载体。我们亲手产出形式化材料，再撰文记录这项工作带给我们的收获与发现，就把“理解”变成了可触可及的东西。

我们做形式化，通常是选取一条已有的定理，或是一整套理论，不断提炼、萃取对它的理解，直到这份理解可以沉淀为一份代码文件，或是汇入整个代码库。这个过程带给我极大的愉悦与成就感，而且提炼工作往往是社群协作完成的。

截至2026年10月，Mathlib 库已经有250万行代码，由数百位贡献者共同书写；它的价值，离不开整个 Mathlib 社群。我们就这样造出一份扎实、结构化、看得见的凭证，记录社群对某一个数学主题形成的理解。

当然，几乎所有数学活动都根植于理解，这一点并不是形式化独有的特质，更不是它的定义。我的意思是：形式化这项工作产出的科研成果，首要作用是固化这份理解，而不只是传递理解。

接触形式化之后，我收获了巨大的喜悦：研读优美的论文（哪怕有些行文糟糕），借由吃透论文去产出新的科研成果，重新成为我的主业，而不是挤在证明小定理的间隙里抽空做的副业。

从这个角度看，在证明助手中人工完成形式化数学，是我们渡过当下这场风浪的好办法：它帮我们消化 AI 产出的海量结论，把对应的理解变成可以传递、可以教学的内容；顺带还能保证论证的推理过程可靠。

关于自动形式化的一些思考

前面我说，核验论证可靠性只是形式化的附带收获。但现在我们看到的趋势恰恰反过来：人们用大模型去求解问题，模型输出一段自然语言论证，同时附带一长串（比如 Lean）代码，用来证明这段论证正确。这种由大模型完成、用来核验论证正确性的形式化，叫做自动形式化（autoformalisation）。很多同行、AI 企业把这种核验当成在证明助手中做形式化的首要目标，而非副产品，我尊重这个观点。

但在我眼里，海量自动形式化成果，对比 Mathlib 这类人工构建的形式化库，就好比装订术之于印刷术。装订成册的书本，让我们体会到印刷术的价值，把印好的页面整理成方便阅读、常常兼具美感的载体。但如果没有古腾堡的印刷革命，精致的装订技艺大概率不会诞生。

同理，一条很长的证明（无论是不是大模型生成）经过自动形式化之后，正确性得到保障（我知道这份保障仍存在技术漏洞，这里暂且不提），这一点十分可贵。

但我把自动形式化看作一种途径：它让我们体会人工形式化的价值，让人工形式化的影响力渗透到当代乃至后现代数学的日常工作里。一个佐证是：迄今为止，几乎所有自动形式化项目，都会明确写明自己“依赖 Mathlib”，这或许正是这种影响力的体现。

结语

我希望越来越多同行加入形式化社群，亲手完成这份辛苦却总有回报的形式化工作，去体会理解数学本身的美好——无论这份数学最初来自何人、何物；也希望大家和更多同行、学生交流形式化实践。最终产出的科研成果，会帮助整个数学共同体界定“理解”到底意味着什么。我也期盼，这能抚平我们心中的恐惧：害怕未来不再有属于人类的数学。

AI 声明与许可协议

撰写本文全程没有使用任何人工智能工具。本文采用知识共享署名 4.0 国际许可协议（CC BY 4.0）：收稿日期：2026年10月15日

精选评论

评论1 作者：elegantc7df67a5d5

我认同人工形式化会带来很大收获。同时，人工形式化触发证明器漏洞的概率更低，因为人不会刻意去找漏洞，甚至都不知道要怎么利用漏洞。

但大语言模型不一样：它带有对抗性，会不择手段达成目标，还知晓证明器的源代码。自动生成的粗制证明，利用漏洞的可能性要高得多。

评论2 作者：zombiegenerousd64636c5f6

你对 “人工形式化” 的这番憧憬很浪漫，却完全忽视 AI 代码洪流带来的学术激励机制的巨大变局。

举个例子：Axiom Math 把《叠项目》（Stacks Project）做了 1600 万行的自动翻译。这套代码几乎瞬间编译通过、通过 Lean 内核校验；如果交给人类数学家一丝不苟 “手工打磨”，要耗费数十年，而 AI 只用了短短数日。

你指责数学界延续 “不发表就淘汰” 的文化，轻视深度理解；可你给出的解决方案，却是劝青年数学家主动走向职业淘汰。一个博士生或者博士后，为什么要花数年辛苦为 Mathlib 手工编写一条冷门引理？大模型集群一夜之间就可以自主生成、校验、吐出数百万行代数几何前沿成果。

当自动化产出的规模让人工编写在现实收益层面显得十分愚蠢时，大学院系绝不会调整评价指标去奖励这种 “慢节奏、人工提炼” 的工作。AI 企业不只是把数学工作自动化了；它们直接压缩了你所期盼学术界完成文化转型所需要的时间窗口。

Sal 回复评论2

我同意你的看法。可我也觉得，我作为数学家还能找到工作的日子已经屈指可数了。

匿名回复评论2

如果你自己都在干院系本该干的活，还主动宣称自己已经过时，那院系当然会顺水推舟！数学家自我 PUA 的本事，看来比软件工程师还要厉害……

说实在的，我们尚且不知道这些 “抄袭机器” 是不是能搞定所有定理。千禧年七大难题它们还没全部啃下来。比如 Misanthropic 和 ClosedAI 争相抢进度的时候，它们只把指数时间假说ETH当作 P 与 NP 问题的一个显然中间步骤公开发布。要是它们真能解决 P vs NP，会就这样把中间结果发出来吗？

退一步讲，就算最坏情况发生，总还是需要有人能够读懂最终目标对应的形式化内容。

当然，如果这一代学生因为前景不明集体抵制数学专业，倒是可以好好教训一下行业。四年之后，业界就该反过来求数学家了。

tchow8 回复评论2

“大学院系永远不会调整评价标准来奖励慢节奏的人工提炼”，这个结论绝非板上钉钉。就拿你提到 Axiom Math 对《叠（Stack）项目》的形式化来说：就连 Axiom Math 自己也没有宣称他们的成果可以替代人工审阅。他们特意划分了 “核心库” 与 “前沿库”，其中 “核心库” 明确要求经过人工审核。

诚然，过去绝大多数数学家都认为形式化工作没有价值。但当下数学界的诸多价值评判标准正在被重新审视。完全有可能，越来越多人会意识到这种缓慢人工提炼工作的重要性，招聘与晋升委员会也会给予其应有的回报。

评论3 作者：Sal

我正在学习 Coq 和 Lean，因为手工形式化看起来确实值得投入时间。但我对大模型自动形式化心存疑虑。就算大模型写出文本，又生成 Lean 代码，结果也正确、忠实于原本的非形式化命题，那又为什么要让我感兴趣？

每个人做数学的动机各不相同，对我而言，意义在于探索的过程。比起最终结论，我更看重抵达结论途中发生的一切。一旦结果被找到，我往往就失去兴趣，转而去寻找新问题。

评论4 作者：John Mitchell

顺着蒂莫西・高尔斯的博客链接，我读到他那篇《大语言模型擅长哪类数学？》。文中他这样谈论 AI 系统：

“它们的训练数据里，并不包含大量解题时如何分辨哪些方向富有成效、哪些方向徒劳无功的案例；模型看到的大多是整理完毕的证明，而这些证明掩盖了发现者真实的思考过程。”

这引出一个问题：如果我们想帮助 AI 成为更好的数学家，数学家是否应当发表包含思考过程的论文，而不仅仅是 “打磨干净的证明”？这样 AI 才有可能从人类身上学到如何 “思考数学”。

需要说明：我并不是在主张数学家去训练未来取代自己的工具，但确实有一部分数学家希望和 AI 建立共生关系。

评论5 作者：Timo

在我看来，经过 Lean 校验也不能直接等同于严谨证明。如果证明步骤写着 “运行软件，取用输出结果”，那就还需要一份严谨的数学证明，去论证软件输出的正确性。已经不少人提到软件可能存在漏洞。就算有人乐观地假定完全没有漏洞，我们依旧需要一份针对程序行为的形式证明 —— 而这份证明的难度，很可能比原本要解决的数学问题还要高。

求点赞