陶哲轩：数学不止是证明，我们该如何看待其余部分

菲尔兹奖得主陶哲轩（Terry Tao）在其个人博客上发表了一篇引发广泛讨论的文章，标题直指数学界一个长期被忽视的问题：如果数学远不止于证明，那么我们应当更好地去认可与庆祝证明之外的那些部分。这篇文章在 Hacker News 上获得了 256 个赞和 207 条评论，反映出技术与研究社区对这一话题的高度共鸣。

数学的价值不只在于证明

在大众乃至部分学界的认知中，数学的核心成果往往被简化为「定理及其证明」。一个数学家的贡献，常常以其证明了哪些著名猜想来衡量。然而陶哲轩指出，这种以证明为唯一标尺的评价体系，实际上遮蔽了数学活动中同样关键的其他维度。

证明固然是数学严谨性的最终保障，但它更像是一座冰山露出水面的部分。真正驱动数学进步的，还包括提出好问题的能力、构建有解释力的概念框架、发现不同领域之间的深层联系，以及为复杂现象提供清晰直觉的洞察。这些贡献往往难以用「证明了什么」来量化，却在实质上塑造了整个学科的发展方向。

被低估的数学工作类型

陶哲轩的核心论点在于，数学共同体在文化和激励机制上过度偏向证明，导致一系列同样有价值的工作被系统性地低估。

提出问题与构建概念

提出一个正确的问题，有时比解决它更困难，也更具影响力。历史上许多重大突破，源自某位数学家重新框定了问题本身。同样，引入一个新的定义或概念——比如群、拓扑空间、概形等抽象结构——可能开辟出全新的研究领域，其价值远超单个定理。

历史上最具说明力的案例之一是亚历山大·格罗滕迪克（Alexander Grothendieck）引入「概形（scheme）」这一概念。概形将代数几何的研究对象从具体的多项式方程的解集，推广为更抽象的环的谱，使得数论与几何得以在统一框架下互动，直接催生了怀尔斯证明费马大定理所依赖的现代工具。格罗滕迪克本人并不以「证明了某个著名猜想」著称，而是以「重新发明了数学的语言」留名。类似地，庞加莱提出同伦群的概念、科尔莫哥洛夫公理化概率论，都是「概念构建」价值凌驾于单一证明之上的典型例证，印证了陶哲轩所说的系统性低估问题。

阐释、综述与直觉传递

将晦涩的证明改写为清晰易懂的阐述，把散落的结果整合成连贯的理论叙事，或者提炼出可供他人复用的直觉，这些「解释性」工作对学科的健康发展至关重要。它们降低了后来者的学习门槛，让知识得以有效传播，但在传统学术评价中却常被视为「次要」。

计算、实验与反例

数学中的实验性探索——通过大量计算发现模式、构造反例推翻猜想、验证边界情形——同样是推动认知前进的重要力量。这类工作虽然不总是以优雅证明的形式呈现，却为严谨结果的诞生铺平了道路。

为什么这个话题正当其时

陶哲轩的这篇文章之所以引发热烈反响，与当下 AI 在数学领域的快速渗透密切相关。随着自动定理证明、形式化验证工具（如 Lean）以及大语言模型辅助研究的兴起，「证明」这一环节正越来越多地可以被机器承担或加速。

这就引出了一个深刻的问题：如果机器能够高效地生成和检验证明，那么人类数学家的独特价值究竟在哪里？答案很可能正落在证明之外的那些部分——提出有意义的问题、判断什么值得研究、赋予结果以意义和直觉。在 AI 时代，重新审视并认可这些「软性」贡献，不仅是一个文化命题，更关乎数学这门学科未来的自我定位。

Lean 是由微软研究院开发的交互式定理证明器与函数式编程语言，属于「形式化验证」工具的代表。形式化验证要求数学家将证明的每一逻辑步骤都翻译成机器可检查的形式语言，从而彻底消除人工审阅中可能遗漏的错误。近年来，Lean 4 的生态快速成熟，数学家 Kevin Buzzard 主导的 Mathlib 项目已将大量现代数学定理形式化，DeepMind 等机构也在探索将大语言模型与 Lean 结合，让 AI 自动补全证明步骤。这一趋势意味着「写出严格正确的证明」这项曾被视为数学家核心技能的工作，正在被机器逐步接管。陶哲轩本人也曾公开表示，他预期在不远的将来，AI 辅助工具将能够处理大量常规的证明细节，使数学家得以将精力集中于更具创造性的环节。

社区的共鸣与讨论

在 Hacker News 的讨论中，许多从业者结合自身经历表达了认同。不少人提到，在学术晋升、论文发表和奖项评选中，可量化的定理成果往往更受青睐，而那些花费大量心血写就的优质综述、教学材料或开源计算工具，却难以获得对等的认可。这种激励错位可能促使研究者规避高风险、高价值但难以「计分」的探索性工作。

也有观点认为，问题的根源在于评价的可操作性——证明的对错是二元的、可验证的，而「洞察」或「概念的优雅」则高度主观，难以建立公认的标准。如何在保持严谨的同时，为多元化的数学贡献建立合理的认可机制，仍是一个开放的挑战。

这种激励错位在学术经济学中有专门的讨论，通常被称为「可测量性偏差（measurability bias）」——评价体系倾向于奖励易于量化的产出，即使那些难以量化的贡献对领域的长期健康更为重要。在数学之外，同样的张力也出现在软件工程（写文档与写功能代码的回报差异）、生物医学（阴性结果难以发表）等领域。部分高校已开始尝试将优质教材撰写、数学竞赛培训或开源软件贡献纳入晋升考量，但缺乏跨机构的统一标准使得改革进展缓慢。Hacker News 讨论中也有人指出，同行评审制度本身就预设了「证明」作为核心货币，若要改变认可机制，可能需要从期刊编委会和资助机构的评审标准入手进行结构性变革。

结语

陶哲轩的这篇文章并非否定证明的核心地位，而是呼吁数学共同体拓宽对「数学成就」的理解。在一个证明可以被日益自动化的时代，人类在提问、阐释、联系和直觉方面的独特能力，或许才是数学最不可替代的部分。如何更好地庆祝这些贡献，将是学科文化演进中值得持续思考的命题。