中心命题：Lean 证书让「这个证明没有漏洞」第一次可以由机器独立判定，但「这个证明意味着什么」仍然只能由人完成。数学界在两个月内收到两份方向相反的署名答案，根源不在道德立场，而在于「证明」长期同时承担着担保正确与传递理解两项功能，而技术把它们拆开了。

证据边界：十项结果均未经同行评审；「约 2,000 美元」仅指成功解答所需 token 按 Sol API 价目的折算，不含失败搜索、训练与人工整理成本；Lean 证书只保证推导链条无缺口，不保证命题陈述被正确翻译，也不评价重要性。

OpenAI 十项数学结果不署人类作者，国际数学联盟两个月前刚说相反的话：这不是道德分歧，是「证明」被拆成了两半

先看一个动作。

在 GitHub 上一个叫 ten-proofs 的仓库里，躺着十份 Lean 文件。你不需要懂数学，也能对它们做一件事：把它们交给 Lean 的内核程序，等它跑完。程序会告诉你两件事——每一步推导是否合规，以及文件里还有没有未完成的证明目标。如果两项都干净，它输出通过。

这个动作不需要人读懂任何一行。它是机械的，可重复的，而且陌生人在自己的电脑上跑出的结果和你一样。

这十份文件对应的，是 OpenAI 在 2026 年 8 月 1 日公布的十项数学与理论计算机科学结果。同一天，这家公司在说明页里写下了一句在数学界很少有人这样公开讲过的话：把完全由 AI 系统生成的证明说成人类作者的作品，会同时歪曲系统的贡献和真正人类智力工作的性质。

而在此之前两个月，2026 年 6 月 2 日，一份由 16 人工作组起草、获得国际数学联盟背书的文件——莱顿宣言——写下的是几乎相反的一句：功劳与责任仍然属于数学共同体中的人，不应当给予自动系统。

两句话都以「诚实」为出发点。得出的操作结论完全相反。

十项结果、约 2,000 美元 token、零同行评审

OpenAI 公布的十项结果来自内部版本的 Astra 模型，覆盖高维几何、编码理论、算术电路复杂度、群论、算子代数、量子复杂性、格密码与极值组合。清单里包括：高维球堆积密度上界推进到 Cohn–Elkies 阈值；非 sofic 群存在性的构造；Connes 刚性猜想的反例；置换积的算术公式下界，量级为 n⁴/log n；一般两方量子博弈的指数型并行重复定理；最近向量问题的多项式因子近似难度；以及解决 Erdős 第 183、146、180 号问题的三项组合结果。

流程是这样的：论证由模型生成，人类与同一个模型一起把论证整理成手稿，之后模型把每个论证形式化为 Lean 证书。OpenAI 另外发布了模型「思考过程的叙述」。

有两个数字需要放在正确的位置上。

第一个是「约 2,000 美元」。原文的准确表述是：找到这些问题的解所需的 token 总量，按 Sol API 价目折算约合 2,000 美元。它不包含失败的搜索开销，不包含模型训练成本，也不包含人工整理手稿与形式化的工作量。任何读成「两千美元解决了十个开放问题」的说法，都超出了原文。

第二个是「十项」。原文用语是「解决或实质性推进」长期开放问题。十项的推进程度并不相同，把它们一律称为「解决」是不准确的。

另外一件必须说清楚的事：这十项结果都没有经过同行评审。OpenAI 的页面通篇没有出现同行评审字样，取而代之的措辞是——我们希望数学共同体深入研读这些结果，把它们放回上下文中。

Lean 只担保一句话：这条推导链没有缺口

要理解那两句相反的话为什么会同时出现，得先弄清楚 Lean 证书到底检查什么。

Lean 是一种形式化证明语言。它把数学论证写成计算机能逐步核对的形式：从一组已经接受的公理和已有定理出发，每一步推导都必须符合明确的规则。检查这件事由一个很小的内核程序完成，它不理解数学，只核对规则。如果某个证明目标还没完成，Lean 里会留下一个占位符，检查时一目了然。

所以证书能担保的，是一句很硬但也很窄的话：从起点到终点，这条推导链没有缺口。

它担保不了三件事。

第一，形式化的那句命题，是不是忠实地翻译了自然语言里的那个定理。如果陈述写歪了——比如少了一个条件——机器照样会报告通过。核对翻译这一步，只能由懂那个领域的人来做。

第二，这个定理重要不重要。它属于哪条研究脉络、回答了谁的问题、能不能推广，证书一个字都不说。

第三，论证里有没有可复用的想法。数学史上很多证明的价值不在结论，而在方法。证书只记录步骤，不区分哪一步是灵光。

这就是为什么 OpenAI 要额外发布模型的思考叙述。证书补不上理解，只能再补一份自然语言的东西上去。

而「证明」这个词在数学共同体里，两百年来一直同时承担着这两件事：它既是正确性的担保，也是理解的载体。一个人读完一份证明，同时获得「我确认它对」和「我知道为什么对」。现在这两件事在工程上被拆开了——正确可以外包给机器，理解不能。

两份文件的分歧，就长在这条裂缝上。

莱顿宣言把署名当作责任装置：署名的人要为对错负责，而自动系统不能负责，所以功劳与责任只能归于人。OpenAI 把署名当作过程描述：署名要如实记录论证由谁产出，所以不能把机器的论证记在人名下。然后 OpenAI 用另一句话把责任单独拎了出来——我们参与了手稿整理和 Lean 形式化，并为它们的正确性负责，而数学论证本身由我们的系统生成。

也就是说，OpenAI 把「署名」和「负责」拆成了两件事。而莱顿宣言的整个框架，建立在这两件事绑在一起的前提上。

莱顿宣言列的五项担忧，没有一条是情绪

莱顿宣言不是一份情绪化的抗议。它列了五项担忧，每一项都指向可操作的东西。

可靠性：宣言原文说，当前的自动化技术能产出「看似合理但不可靠甚至错误」的论证，而这些论证很难与正确的数学证明区分开；这些快速进展让现有的评审系统承受越来越大的压力。注意措辞是「承受压力」，不是「已经失效」。

署名：在已发表作品上训练的模型，输出中经常没有恰当引用它所综合的那些人类工作。

访问：宣言写道，这会使那些无法获得相关技术、或不愿使用由价值观不同的组织所控制的技术的研究者处于不利地位。它还有一句更根本的话——数学论证被认为是透明的、可被独立验证的；它们可以极长、极难，但原则上理解它们不应当需要任何专有知识或专有设备。

自主性：技术公司越来越深地介入数学研究，带来的风险是研究问题会因为「适合被自动化」而被优先，而不是因为专家判断它更深刻。

宣言给出 23 条编号建议，其中面向个人数学家 11 条、面向数学组织与非营利资助方 8 条、面向政策制定者 4 条。它没有强制力。它的分量来自国际数学联盟的背书，以及 16 位来自华盛顿大学、爱丁堡、哥伦比亚、剑桥、牛津、西北大学、苏黎世联邦理工等机构的起草者。

还有一个反向的证据，同样应该摆出来。2026 年 5 月，OpenAI 公布了 Erdős 单位距离猜想的一个反证。此后至少有五篇论文在这个结果上继续推进，都能在 arXiv 上查到编号——其中一篇的结论是实数上的和积猜想不成立。这说明「人类社群接住机器结果并把它变成新研究」这件事确实发生过。但样本是一个案例，不是一种规律。

科学这层最硬，制度这层最空

把这件事拆成四层，会看得清楚一些。

科学上可行吗？ 十项结果都附有可机器检查的 Lean 证书。就「推导链无缺口」这一条而言，答案是明确的。但「命题陈述是否忠实」这一层，需要各自领域的专家逐个确认，目前还没有完成。

工程上可复制吗？ 这里的复制不是指别人能不能跑通证书——那很容易。而是指别的团队能不能用同样的方法产出新的结果。这依赖内部版本的模型、依赖具体的提示与搜索策略，都没有公开。

经济上可承受吗？ 「约 2,000 美元」这个数字如果指的是完整成本，那么答案是惊人的便宜。但它不是。它是成功 token 的零售折算价。真实的搜索成本、训练成本、以及人类整理与核验的时间，都不在里面。在这些数字公开之前，「便宜」这个判断不成立。

制度上可接受吗？ 这一层最不确定，也正是两份文件在争的东西。期刊要不要接收一份「论证由模型生成、公司为正确性负责、无人类作者」的稿件？评审要读什么？如果证书通过而没人读懂论证，这个结果算不算进入了数学？现在没有答案。

做「语境化」的那批人，没有署名也没有预算

这场争论里有一类人几乎不出现在标题里，但承担了最实际的变化。

是做「语境化」的人。把一个孤立的结果放回学科脉络，指出它和哪条线索有关、它意味着什么、下一步该问什么——这项劳动一直存在，一直重要，但在现行的论文计数体系里几乎不产生署名。OpenAI 那句「我们希望数学共同体深入研读这些结果、把它们放回上下文」，读起来是一句客气话，实际上是把一项没有署名、没有计分、也没有预算的工作，交给了外面的人。

莱顿宣言里有一句话点到了这件事的经济基础：大学预算压力可能导致研究者与技术公司之间形成不对称的合作。谁有算力、谁有时间、谁能承担「读完一份自己不会因此获得任何署名的证明」的机会成本，从此变成了实实在在的分层。

还有期刊评审。他们要处理的东西变多了，而判断的依据变复杂了——证书通过意味着什么、不通过意味着什么、翻译对不对由谁确认，这些都还没有共识。宣言用的词是「压力」，这个词很克制，也很准确。

必须并列另一种解释：这两份文件的分歧，也可以完全不用认识论来讲。公司需要为产品能力背书，学界需要保护自己的评议权与议程设定权，双方所说的「诚实」各自服务于各自的位置。这个解释是成立的。它和本文的说法并不冲突——利益差异解释了他们为什么在此刻表态，结构性的拆分解释了他们为什么各自都能自洽。

能验证，和能理解，从此不是同一件事

回到那个可以在自己电脑上重复的动作。

你把十份 Lean 文件交给内核程序，它跑完，输出通过。这一刻，一件在数学史上从未如此干净地发生过的事情成立了：一个陌生人，不理解这份证明的任何内容，却能独立确认它没有漏洞。

莱顿宣言里那句关于透明性的话说得很好——数学论证可以极长、极难，但原则上理解它们不应当需要专有知识或专有设备。Lean 证书恰好实现了这句话的前半段：验证不再需要专有知识。它同时也让后半段变得刺眼：能验证，和能理解，从此不是同一件事了。

数学共同体接下来要决定的，不是要不要用这些工具。是要不要给「读懂」这件事重新定一个位置——在一个正确性已经可以外包的世界里，谁来做理解，以及这项劳动值不值得一个名字。

参考资料清单

• 《Ten advances in mathematics and theoretical computer science》，OpenAI，2026 — https://openai.com/index/ten-advances-in-mathematics/
• 《莱顿宣言》，2026 — https://leidendeclaration.ai/
• Lean 证书仓库 openai/ten-proofs，OpenAI — https://github.com/openai/ten-proofs
• 《国际数学联盟对莱顿宣言的背书函》（IMU AO CL 8/2026），国际数学联盟，2026 — https://www.mathunion.org/fileadmin/documents/2026-06/IMU_AO_CL_8_2026.pdf
• 《Erdős 单位距离猜想反证公告》，OpenAI，2026 — https://openai.com/index/model-disproves-discrete-geometry-conjecture/
• 后续论文 arXiv:2605.28781，arXiv，2026 — https://arxiv.org/abs/2605.28781
• 后续论文 arXiv:2606.13619v2，arXiv，2026 — https://arxiv.org/abs/2606.13619v2
• 后续论文 arXiv:2607.05374，arXiv，2026 — https://arxiv.org/abs/2607.05374