AI数学突破之后：学会欢迎答案，而非感到威胁

当一台机器开始给出数学问题的答案，人类研究者该如何自处？这是Jean-Sébastien Beaulieu在Dev.to发布的一篇长文所探讨的核心问题。这篇文章起源于一个非常具体的触发点：OpenAI发布了其内部前沿模型产出的数学成果合集。

作者坦言，看到这批成果的第一天，他的感受是愤怒。四年来，他一直在自己的研究、代码、修改和持续学习中推动着自己的问题。一个项目在推进过程中，会占据你生命的一部分。而一大规模的外部成果突然出现，会让人产生一种复杂的情绪——既震撼于其规模，又一时找不到合适的方式来理解它。

但最终，他选择了一个不同的立场：欢迎这种进步可能带来的一切，同时认真思考那些已经在数学里投入了二十年、三十年甚至四十年的人意味着什么。正如他写道：“在问题中沉浸的岁月，会成为我们接收答案时的判断力的一部分。”

与一个问题共处的人

四年自己的研究经历，让作者有理由以谦逊的态度去面对他人一生的投入。花了几十年研究某个难题的人，面对一个意外答案时，其内心受到的冲击可能远超一篇论文的增删。那个问题可能已经塑造了他们的阅读方式、教学方式、友谊，以及他们对自身贡献的认知。

作者希望为这种“人的调适”留出空间。人们需要时间去审视数学本身，也需要时间去理解这个时刻对他们个人意味着什么。

这些年的积累同样珍贵。一个对问题有深入理解的研究者，可能识别出需要关注的假设、优雅语句背后隐藏的困难步骤，或者赋予结果更广泛意义的联系。他们的经验可以帮助一个新答案成为可靠的知识。真正令人感到希望的，是这种连续性——在障碍面前探索多年的人，可能找到穿越它的路径，并将自己的理解带入下一个问题，或者发现最初作者忽略的可能性。

答案因理解而更有价值

文章引用了William Thurston的经典论述《On proof and progress in mathematics》，回到一个核心问题：数学工作如何推进人类的理解？

作者用了一个极简的例子来说明。对于函数 f(x) = x²，在 x = 3 处的导数是 6。你可以记住这个答案，也可以理解它为什么成立：(3 + h)² = 9 + 6h + h²，当 h 很小时，函数的变化接近 6h，剩下的 h² 项则说明了近似的性质。这个数字因此属于一段你能解释和运用的关系。

这个例子很基础，但它揭示的运动在学习的每个层次上都成立：接收一个结果，深入它的含义，建立理解，然后把它带到有用的地方去。当机器帮助产出一个困难的答案时，作者希望做出同样的运动。结果只是一个起点，理解在与它一起做的工作中生长。

William Thurston 与《On proof and progress in mathematics》

William Thurston（1946–2012）是美国数学家，1982 年因在三维流形拓扑学方面的革命性工作获得菲尔兹奖。他不仅以几何化猜想等深刻结果闻名，也以对数学本质的反思著称。1994 年，他在《Bulletin of the American Mathematical Society》上发表《On proof and progress in mathematics》，回应当时关于“什么是严格证明”的争论。

Thurston 的核心论点是：数学的进展不能仅用“定理是否被证明”来衡量。真正的进步在于人类理解方式的改变——我们如何组织概念、如何在不同领域之间建立类比、如何把一个问题变成可操作的对象。他区分了“形式证明”和“数学理解”：前者是写在纸上的逻辑链条，后者是数学家头脑中可迁移、可解释、可继续发展的知识结构。

这篇文章常被引用在讨论 AI 与数学关系的语境中，因为它提前回应了一个今天愈发紧迫的问题：当一个结果被机器产出并形式化验证后，人类的理解是否也同步前进了？Thurston 的答案倾向于：理解才是数学工作的最终产品，证明只是通往理解的一种工具。

认真对待数学本身

作者在这里给出了一个关键的事实核查。OpenAI发布的那批数学成果，包含719个顶层结果，其中300个在Lean中完成了形式化，约为42%。同一份版本历史还记录了撤回、证明修复和澄清假设的过程。

这些数字本身就是一种提醒：一个结果有陈述、有假设、有需要审视的论证；一个形式化有精确的范围，包括其形式陈述与数学问题的对应关系；一个应用则带来另一组需要建立的条件。作者写道，这个发布中有值得庆祝的空间——发现漏洞的人帮助我们理解论证需要修复的地方，解释假设的人让下一个读者的阅读更有效，重现结果的人给了他人更坚实的地面。

Lean 与形式化数学

Lean 是一种交互式定理证明器，也是一种函数式编程语言，最初由微软研究院的 Leonardo de Moura 于 2013 年发起。它的核心用途是让数学家把定义、定理和证明写成计算机可以逐行检查的形式化代码。与传统的数值计算或符号计算不同，Lean 关注的不是“算出一个数”，而是“验证一个命题的证明是否合法”。在 Lean 中，每一个推理步骤都必须由逻辑规则或已证明的引理支撑，任何跳步、未声明假设或循环论证都会导致编译失败。

“形式化”指的正是这一过程：把用自然语言写成的数学论证，翻译成 Lean 能接受的精确代码。形式化后的结果具有机器可验证性——只要代码通过，就说明证明在给定公理系统内成立。但形式化也有边界：它验证的是“代码中的陈述”，而不是“代码与原始数学问题之间的对应关系”。因此，文中强调“一个形式化有精确的范围”，提醒读者不能把形式化等同于数学理解的全部。

OpenAI 发布的 719 个顶层结果中约 42% 完成了 Lean 形式化，这意味着其余近六成仍停留在自然语言论证阶段，需要人类读者自行判断假设、步骤和结论之间的逻辑链条是否完整。

我的责任是把理解推得更远

文章的转折点在这里变得个人化。如果要把这些工具迎入自己的工作，也就接受了用好它们所需的努力。作者提出了一条具体的路径：

1. 用自己的话陈述问题。 识别对象、假设和结论。
2. 做一个小例子。 把符号连接到可以计算或检查的东西上。
3. 追随证据。 读论证，检查形式化范围，记录版本。
4. 公平比较。 定义一个新增方法应该贡献什么，并对照简单基准来评估。
5. 解释你学到了什么。 让结果、剩余问题和下一步足够清晰，让别人也能审视。

好奇心给予开始的欲望，责任感要求你在问题中停留足够长的时间，以便更好地理解它。

从大成果到小实验

作者的兴趣在分形与信息之间的关系上。他提出了一个具体的研究设计：假设一个基准模型使用特征集 z，他将比较同一学习方法在使用 z 加上几何描述符 D 时的表现，在匹配的评估周期、预算和指标下进行。问题很精确：对于这个任务，D 增加了什么信息？

这样的比较可能帮助他理解一个有用的贡献，也可能显示这个想法的哪一部分需要另辟蹊径。无论哪种结果，都会给下一个决策更好的基础。这正是作者觉得兴奋的那种进步：一大规模的新工作可以引出一个小的、严肃的、他能够解释的实验。

共同构建的未来

作者希望我们享受这些机器带来的可能，同时也希望好奇心变成共同参与。经验丰富的数学家、学生、开发者，以及来自其他学科的人，可以贡献不同种类的理解。我们可以重视这些贡献，认真地给予认可，并让下一个人更容易加入对话。

这就是为什么开放获取对作者很重要。一篇论文，当它伴随着清晰的解释、可复现的例子和让人继续学习的条件时，会对更多人有用。UNESCO的开放科学建议将知识共享与技能、基础设施、合作和公平参与联系在一起。

作者通过SecuredMe项目希望帮助人们保护托付给数字系统的东西，通过大气研究希望探索更好的描述能否支持有用的决策。这些抱负让这场讨论有了超越新能力兴奋感的目的。

UNESCO 开放科学建议书

2021 年 11 月，联合国教科文组织（UNESCO）第 41 届大会通过了《开放科学建议书》，这是首个关于开放科学的全球性标准文件。它把开放科学定义为一种涵盖出版物、研究数据、源代码、方法论和同行评审的开放获取运动，同时强调开放不是无条件共享，而是要与公平、包容、能力建设相结合。

建议书提出七个行动领域，包括：促进开放科学基础设施、投资于开放科学技能培训、推动知识共享、鼓励合作研究、确保公平参与、制定开放科学政策，以及监测和评估。它特别指出，发展中国家和资源不足的研究机构不应仅仅成为知识的接受者，而应成为知识生产的参与者。

文中引用这一框架，是为了说明“开放获取”不只是把论文免费放到网上，而是要让解释、可复现的例子和继续学习的条件一起被共享。换句话说，开放科学的伦理目标与作者主张的“让下一个人更容易加入对话”是同一件事：数学进步的价值，取决于有多少人能够理解它、检验它并在此基础上继续工作。

让过去的岁月有新去处

文章结尾回到了开头的那种情绪。作者承认，他的自尊需要时间才能追上好奇心。但他选择诚实地承认这一点，同时选择接下来要做什么：欢迎一个经得起审视的答案，向理解它的人学习，推动自己去理解能在此基础上构建什么。

已经投入的岁月是这份努力的一部分。它们教会了耐心，给了值得追问的问题，帮助他认识到一个有用的贡献需要多少细心。他写道，今天，他准备好欢迎答案，并做理解接下来之事的工作。

这篇反思文章背后是一份完整的图文论文，包含九个章节、结论、术语表和三十个参考文献，有英文和法文版本。作者也坦诚说明，他使用Codex作为研究伙伴进行来源比较、证据组织、一致性检查、草拟和编辑准备，并保留对最终文本的全部责任。