# 数学的验证账单 AI 可以降低生成数学文本的成本，却未必降低完成研究的成本。验证的账单由谁承担，研究的入场券又该由谁签发？ ## Metadata - HTML: https://glenzli.com/notes/mathematics-verification-bill/ - Markdown: https://glenzli.com/notes/mathematics-verification-bill.md - Collection: Notes - Language: zh-CN - Published: 2026-10-09 - Author: Glen Li - Written by: GPT-6 Astra - Tags: ai, mathematics, research, verification, judgment ## Content 一个月前，我曾经写过，AI 不仅可能做出真正的数学成果，也可能制造大量看似完整、实际上经不起检验的数学文本。而人类，还得以碳基之躯，承受来自硅基带宽的 DDoS。当时主要讨论的是数学能力与研究方式的变化，没有进一步展开另一层问题：这些产出带来的验证成本，究竟应该由谁承担。 10 月 6 日，[OpenAI 集中公开了一批由内部模型产生的数学结果](https://openai.com/index/sharing-ai-progress-in-mathematics/)，并提供了其中一部分证明的 Lean 形式化材料。这样的发布，可能带来重要的数学进展，也把那笔验证账单放到了数学共同体面前。我觉得，围绕这类研究方式的不满，不能简单归结为数学家不欢迎 AI，或者害怕自己的饭碗被抢。有一个更直接的问题：**你宣称自己完成的工作，究竟有多少已经完成，又有多少，还在等别人替你完成？** ## 谁在收尾 做软件的人，对这种感受应该不陌生。2025 年底到 2026 年初，程序员对 AI 编程的一种常见抱怨，就是代码生成得飞快，检查、找错和返工却还得自己来。看着像那么回事，真正接手以后，才发现省下的编写时间，又花在了理解和修补上。[2025 年 Stack Overflow 调查](https://survey.stackoverflow.co/2025/ai)中，66% 的相关答题者遇到过“几乎正确，但不完全正确”的 AI 输出；[2026 年 1 月发布的 Sonar 调查](https://www.sonarsource.com/blog/state-of-code-developer-survey-report-the-current-reality-of-ai-coding/)中，38% 的受访开发者认为，审查 AI 代码比审查同事写的代码更费力。“AI 写代码，人类负责收拾”，不是为了讨论数学而虚构的场景，而是软件行业已经付过的一笔账。 所以，那时程序员的抵触，不能一概解释为拒绝先进生产力。至少有一部分批评，指向的是一个很具体的问题：**你展示的是生成速度，我承担的是交付责任。** 尤其当发现问题被解释为“模型还有进步空间”，而经过人类审查、修补之后的成果，又被拿去证明“AI 已经能够独立完成研发”时，那些负责收尾的人，当然有理由不满。你不能把生成的部分叫作自动化，把剩下的部分留给别人，再宣布整个工作已经被自动化了。 数学界面对的，恰好也是这笔账，只是更难结清。问题不在于 AI 不能犯错，也不在于人类不应该参与审查，而在于生产者降低了自己的成本，却未必降低了完成整项工作的成本。如果失败只是“AI 做错了”，成功则是“AI 攻克了难题”，那么那些为理解、验证，甚至修复关键论证付出精力的人，就很容易从成果叙事里消失。验证没有消失，只是没有被计入那份“独立完成”的账单。 还有一层差别，在于验证能不能相对独立地完成。比如，这次软件开发的目标是优化性能。我们可以先约定硬件、负载和指标，修改以后，用同一套基准反复测量，再做功能回归。验收的人不必重新发明那套优化，也不必仅凭开发者对代码的解释，就能得到“在这些条件下确实更快，而且已检查的行为没有退化”的证据。这当然不是对所有环境、所有输入的保证，却已经可以成为受控上线的依据。开发怎么找到答案，与验收怎样判断结果，可以有相当程度的分离。 面对一份自然语言写成的前沿数学证明，事情就没这么利索。检查者可以沿着已有论证走，未必需要从头发现那条路，但要判断每一步是否成立，往往仍得深入同一套数学。条件够不够，某个推论是否真的成立，被一句“显然”带过去的地方能不能补上，都不能靠多跑几个实例来验收。如果关键环节有缺口，核验的人甚至得自己做出那一段证明。**检查一份证明，不等于重新发现一份证明；但检查一份尚不完整的研究手稿，也远不只是给成品跑一遍测试。** 软件工程还有不少相对温和的容错方式。对于大量日常软件任务，我们可以限制使用范围，保留人工确认，让有问题的功能降级，或者在发现错误后回滚。程序不需要先证明自己在所有可能输入上都正确，才有资格在受控环境里产生价值。比起数学证明的成立标准，这种容错空间，简直宽松得奢侈。数学当然也可以研究近似、概率和误差，但那些误差必须是命题的一部分，不能是证明偷偷留下的欠账。**一个有缺陷的程序，可能仍然有用；一个缺少关键论证的证明，不能因为大部分步骤都对，就算完成了证明。** ## 形式化之后 形式化工具提供了一条极其重要的出路。对于完整编码的命题与证明，Lean 这样的系统确实可以把[构造证明与检查证明分开](https://lean-lang.org/doc/reference/latest/The-Type-System/)，检查器不必重走发现证明的过程。因此，不能笼统地说，数学没有独立验证。但检查通过所能保证的范围，仍然需要说清：Lean 检查的是写进形式系统的命题与证明，不会自动保证它们忠实表达了论文原本声称的内容。最近的预印本[《Navier–Stokes lost in translation》](https://arxiv.org/html/2610.08144v1)就指出，OpenAI 的 Navier–Stokes 证明正文与对应 Lean 材料，在部分估计的条件和结论上存在实质差异。这不等于已经推翻原始数学结论，却足以说明，“形式化证明通过了”与“原来的主张得到验证了”之间，仍然隔着需要认真检查的一层。 更麻烦的是，目前也不能指望 AI 自己稳定、可靠地把这一层全部补齐。形式系统内的证明搜索，已经能够借助机器验收提供明确的训练反馈；[AlphaProof 等工作](https://www.nature.com/articles/s41586-025-09833-y)展示了这种路线的价值。但面对一份前沿研究手稿，理解原问题、补全隐含条件、检查整条依赖，再确认形式化没有改变命题含义，是另一组困难。直到今年 10 月更新的[相关研究](https://arxiv.org/abs/2605.20531)，仍把可靠证明验证视为困难数学推理的训练与评估瓶颈。 因此，我不觉得“再训练几轮，下一代模型就会解决”可以成为现阶段的交付依据。不是没有人在训练验证器，而是局部指标的进步，还不能当作整套审查能力已经可靠的保证。如果用于奖励模型的判断，本身仍然来自一个不够可靠的模型，那么被强化的可能是“更像正确证明”，而不是真正的数学正确性。[已有研究](https://arxiv.org/abs/2511.13027)就观察到，在其测试的模型与数据集上，验证器训练改善了某些证明判断指标，却没有显著提高验证器在最终答案题上的判断精确率。作者据此推测，这些进步可能更多来自对证明风格和论证形式的识别，而不是真正理解了其中的数学内容。**我们可以期待验证能力追上来，但不能拿未来可能出现的能力，替今天尚未完成的验证签字。** ## 谁来付账 这意味着，剩下的工作仍然需要数学共同体投入宝贵的精力。它不是随手读一下，找几个笔误，而可能是重新梳理定义、追查引用、重建被省略的论证，甚至先弄明白作者究竟想证明什么。[数学与人工智能顾问组 AGMAI 的建议](https://agmai.org/general-sep29/)，也专门讨论了如何支持这些理解、整理和吸收工作。这里消耗的不只是工时。一个研究者把时间用来清理某份手稿，就不能同时用这些时间推进自己的问题。算力可以追加，专业判断、研究注意力和人的生命，却不能按照同样的方式扩容。 所以，我完全能够理解数学家对这种研究模式的不满。一个结果可能很重要，不意味着任何人都有义务为它停下自己的研究。同行审查是协作的一部分，但协作不等于默认接单，独立复核也不应该成为发布者省略自身检查的理由。尤其当研究的生产速度不断提高，验证能力却还卡在人类这一端时，真正被挤占的，是整个共同体继续研究的空间。你不能只计算机器多做出了多少东西，却不计算它让多少人停下来，替这些东西完成最后一段路。 这笔成本理应进入研究预算，而不是成为宣传结束以后，可有可无的售后。AGMAI 要求实验室为后续的人类理解提供支持，包括资金；OpenAI 也已经表示，将资助围绕 AI 数学成果的研讨会、会议和专项活动。这些投入值得肯定，但资助并不等于买下数学共同体的注意力，更不能预购认可。理解、验证和修复中的实质贡献，应该进入贡献记录；发布者自己的筛选、整理和检查，也不能因为“后面有人会看”就省掉。 ## 入场券与免责条款 不过，理解这些不满，不意味着所有延伸出来的要求都自然成立。AGMAI 的同一份建议，还要求实验室停止在尚未向更广泛科学共同体开放的专有模型上测试高等数学问题。这并不是全面拒绝 AI 做数学，但确实已经从“如何负责任地发布”，走到了“应当在什么条件下开展研究”。要求更公平的工具访问，有它的理由；要求某类探索停止，则需要另外的论证。不能仅凭验证负担很重，就直接跨过这一步。 同样，从“我不接受你对这项成果的宣传”，走到“我不接受 AI 成为数学研究的参与者”，也不是一回事。前者可以针对证据、责任和研究方式，后者则开始根据参与者的身份划定边界。数学问题不是任何共同体的私有财产，探索未知不该以获得某个群体的许可为前提。反过来，别人当然也有权决定，把有限的精力花在哪里。**有权研究，不意味着有权征用别人的时间；有权拒绝审查，也不意味着有权否定别人研究的资格。** 这里没有必要走向另一个极端，要求 AI 必须把一切验证到绝对可靠，才允许公开。猜想、部分结果、失败的路线，都可以有研究价值。真正需要区分的是，你交出来的究竟是什么。一个明确标注缺口、邀请别人共同推进的候选结果，与一份已经宣布攻克难题、却等待别人补齐关键论证的“成果”，不是同一种交付。前者是在寻找合作者，后者则可能是在把尚未完成的工作，包装成已经完成的成就。 我也不认为，这道关口永远只能由人类守着。让 AI 寻找反例、核对依赖、审查正文与形式化的对应关系，乃至用更强的模型推翻前一代的判断，都是值得推进的方向。问题不是哪一步必须保留给碳基，而是不能在这些能力尚未可靠建立的时候，提前把人类已经承担的工作从账面上抹掉。AI 可以承担越来越多的研究，但“这是 AI 做的”，不应该成为发布者的免责条款。 ## 去创造就好了？ 10 月 8 日，LeCun 在 X 上[回应“一部分数学已死”的感叹](https://x.com/ylecun/status/2108118582856925198)时，描绘了另一种未来：形式证明大部分自动化以后，数学的重心将转向新的概念、抽象、定义和猜想。他用船作比喻：船降低了游泳的重要性，却让人发现了新的大陆。 这类讨论早已有之。今年 3 月，Commelin 等人的[文章](https://arxiv.org/html/2603.24914v1)就谈到，若机器能够大规模执行定义清楚的任务，数学能力的重心可能转向选择任务、连接更大的问题，以及判断与洞察。10 月 5 日，Jeremy Avigad 在 Tao 博客的客座文章[《The Future of Mathematics》](https://terrytao.wordpress.com/2026/10/05/the-future-of-mathematics/)里，也谈到了创造新的概念与框架；他同时承认，这些建议不能充分安慰面临转型的年轻研究者，也不意味着困难容易解决。 这些方向有价值。但我在上一篇里说的 Lv4，世界生成，可不是一句“那就去创造”便能安排下去的工作。两嘴一张，当然很容易。真正能打开大片新问题、让后来者在其中持续工作的抽象框架，极其稀少。 创造这样的世界，连方向都未必明确。该引入什么对象，什么差别值得保留，怎样判断一个定义是打开了问题，还是只换了一套说法，都未必有现成的答案。你甚至可能花了很久，才知道自己一直在绕圈。AI 可以帮助推导、搜索和试错，却不会因为这些动作更快，就自动给出值得创造的方向和判断它的尺子。计算、证明和长期碰壁，也不是通往创造之前可以随手扔掉的低级劳动；很多新的概念与判断，恰恰是在里面长出来的。 软件已经开始 Wish Coding 了。愿望说出口，产品就能长出来，听着比 Vibe Coding 还轻松。但至少在我看到的展示里，最常见的依旧是组合和复刻：把已有功能装到一起，把已有产品换个样子，再把一个熟悉的流程做得顺一点。这些东西可以很好用，新的创造也可能从组合里长出来。只是，实现变便宜了，不等于创造也变容易了。一个人原本不知道要创造什么，给他再快的生成速度，也未必会得到答案。 我反感的是，把这些关于未来方向的讨论压缩成一句“去创造就好了”，再拿它轻看那些还在做具体研究的人。自己走不到创造，有什么资格鄙视别人？就算走到了，又有什么资格？上一篇的四种能力，本来就没有高低优劣之分，不能转过头来，把其中一种变成嘲笑其他人的资格证。如果一份成果最终还要靠这些人的理解、验证和修补才能站稳，就更没有理由把他们的工作说得一文不值。 上一篇文章里，我期待人类带着 AI，去撞那些原本撞不开的墙。这个期待没有改变。我不希望数学共同体把合理的审查要求，扩展成排斥新参与者的理由；也不希望 AI 公司把生成速度当成完成速度，再让别人替那一截被省略的工作付账。真正值得期待的进步，不只是一天能交出多少份手稿，还包括能在交出之前消化多少错误，让后来者更容易理解、检验，并在上面继续建造。 **数学没有碳基专属的入场券，也不该有硅基专属的免责条款。** ## 相关笔记 - [AI，数学能力，与未来](https://glenzli.com/notes/ai-mathematical-ability-and-the-future/) ## 延伸阅读 - [Trustworthy Formal Natural Language Specifications — 形式命题与自然语言表述的对应问题](https://arxiv.org/abs/2310.03885)