重新定义数学价值：倡导有动机的解释的必要性

证明作为理解代理的危机

在人工智能生成证明的时代，传统数学成功的衡量标准——解决开放性问题并生成证明——正逐渐无法充分反映数学的真正目标：推动人类理解。当机器能够生成证明却无法提供直观洞察时，这种证明作为人类智力进步衡量标准的价值便被削弱了。

为应对这一问题，Grant Sanderson 提出，数学界应正式定义并奖励「有动机的解释」。这一转变将使领域关注点从证明的二元输出（正确或错误）转向使数学概念清晰且直观的过程。

定义「有动机的解释」

有动机的解释在结构、目标和有效性度量上与形式化证明有根本区别。虽然证明旨在说明定理为何为真，但有动机的解释则旨在阐明为何提出该定理是恰当的，以及它如何融入更广泛的背景中。

证明与有动机解释的关键区别

特征	形式化证明
定义的位置	定义出现在开头；构造在分析其性质后才引入。
逻辑路径	每个断言必须从前一步必然推出。
主要目标	证明某个定理为真。
验证方式	二元判断（正确或错误）；可由 Lean 等工具验证。

Sanderson 指出，「发现虚构」——Michael Nielsen 提出的一种叙事风格——是这一类别的典型范例。在发现虚构中，读者跟随一系列简单但错误的解决方案，识别其失效之处，并逐步修正，直到最终获得正确的洞察。

数学阐述的典范

历史上，高价值的阐述常被视为「不产生学分的活动」，通常只有在数学家达到巅峰地位（如获得菲尔兹奖）后才会进行。Sanderson 认为，这类工作应成为职业认可的组成部分，而非其附属产物。

《普林斯顿数学指南》：由 Timothy Gowers 编辑，该书为数十个活跃研究领域提供了深刻的直觉和动机，其清晰度堪比黑板上的对话。
Bill Thurston 的工作：在他的论文《论数学中的证明与进展》中，Thurston 认为数学家的核心成就是推进人类理解。他的影片《Outside In》可视化了球面翻转，将这一发现的影响从单一证明（0 到 1）扩展为广泛的人类参与（1 到 N）。
Timothy Chow 的「开放阐述问题」：Chow 提出了「开放阐述问题」的概念，其目标是将某一主题解释得完全清晰明了。

人工智能对数学实践的影响

近期的发展凸显了证明存在与理解存在之间的日益扩大的鸿沟。例如，Erdős 问题 1196 的解决涉及与 GPT-5.4 Pro 的交互。尽管 AI 提供了证明，但人类数学家（包括 Terence Tao）仍需随后撰写论文，扩展并 contextualize（上下文化）关键思想，使其对人类可读且可用于其他问题。

这表明，未来每个 AI 生成的证明都将作为「未解决的阐述问题」诞生，从而对人类翻译机器验证的真理为人类可理解的洞见产生巨大需求。

学术激励机制的建议转变

为提升有动机解释的地位，Sanderson 建议对数学的学术与职业结构进行若干实际调整：

教学方式转变：博士导师可要求学生以讲座形式向同侪和教师展示解决方案，重点在于解释直觉，而非仅提交书面解答。
新基准设定：领军人物可列出现代版的希尔伯特问题，特别标注重要领域中的「未解决的阐述问题」。
机构认可：招聘与终身教职决策可更重视高质量教材和阐述性工作的贡献，类似于 AMS Steele 奖（表彰阐述），但适用于早期职业研究者。
专门出版平台：设立专注于使研究成果在社区内更广泛被理解的期刊（如 Mathematical Discourse）。

社区观点与反驳意见

从业者与观察者之间的讨论揭示了对理解的渴望与职业数学经济现实之间的张力。

「实用性问题」

一些批评者认为，如果 AI 最终能像生成证明一样高效地生成自然语言解释，将目标转向「解释」可能并非人类数学家可持续的防御机制。一位评论者指出：

"最好的有动机的解释将由 AI 生成，它对主题和你有深刻理解，这种理解远超任何其他人类，并能在解释过程中与你互动。"

「支线任务」的丧失

有人担心，依赖 AI 快速解决问题将消除「支线任务」——即在艰难证明过程中产生的旁支发现——这些发现往往催生全新领域（例如，费马大定理的求解过程推动了椭圆曲线密码学的发展）。

职业角色的转变

有人将当前数学状态与软件工程行业类比，过去「写代码」是主要任务，如今已转向系统设计与代理协调。担忧在于，即使职业角色得以保留，「工作的质感」和解决问题的技艺也可能随之消失。