AI 时代的数学

解释的作用 vs 仅仅正确

• 核心争论：如果一个结果没有任何人能给出清晰、专家级的解释，它是否还应该可以发表？
• 支持者认为：解释本就是研究数学的全部意义；否则别人无法在其基础上继续发展，数学家之间的“对话”也会中断。
• 批评者认为：这等于人为把数学限制在人的认知极限之内，并忽视那些真实、重要或在实践上有用、但难以解释的结果。

形式化验证、信任与不透明证明

• 许多人预计，在 proof assistants 中经过形式化验证的证明会变得如此庞大而复杂，以至于没有人能完整理解它们。
• 有人认为这完全可以接受：你只需要信任一个很小的 kernel 和定理陈述，而不必信任整个推导过程。
• 也有人指出，prover 中的漏洞和被利用的案例说明，我们仍然需要独立理解以及多个系统相互印证。

数学的价值与目的

• 一种观点：数学本质上关乎人的理解和共享的心智模型；无法理解的证明几乎没有数学价值。
• 另一种观点：数学关乎客观真理；一个被验证的定理即使人类无法跟上其证明过程也仍然有价值，尤其是在它支撑了应用时（例如密码学、算法）。
• 对于“只知道一个命题为真（却不知道为什么）”本身是否有用，也存在分歧。

AI 对数学实践与职业的影响

• 许多人认为，不使用 AI 会在职业上处于劣势；AI 已经在参考文献、形式化以及常规证明搜索方面提供帮助。
• 有人预见会出现分化：一个“AI 数学世界”快速前进，而一个“人类数学世界”只研究少量经过筛选的子集。
• 也有人担心 AI 会向该领域灌入大量形式上正确但价值低的结果，淹没人类注意力。另一些人则预测，这反而会抬高而不是降低雄心标准。

发表、期刊与激励机制

• 有建议认为：期刊或招聘委员会可以要求作者进行清晰的报告，以此作为理解力筛选。
• 反驳意见：期刊和审稿人已经不堪重负；解释并没有得到足够回报，因此如果激励不改变，不可理解但已验证的工作可能会占上风。

类比与更广泛的影响

• 将象棋引擎视为“ground truth”式的走法，与将证明视为理解工具；大家对这一类比能成立到什么程度存在分歧。
• 几条评论推测，未来人类的智力劳动可能会变成可选的或娱乐性的，这引发了关于能动性、价值，以及谁在控制 AI 生成知识的问题。