数学之后
内容提要
陶哲轩博客的客座文章讨论了OpenAI宣称用AI解决纳维-斯托克斯问题。作者认为AI给出的是“答案”而非真正“解答”，因为数学证明既需逻辑正确，也需人类可理解。数学不仅是解题，还包括发展理论、理解世界和培养社群。应将AI视为助手而非对手，真正的问题是数学应追求什么目标。
延伸解读
逻辑证明与可理解证明的分离
文章指出，数学证明有两种含义：逻辑有效性和人类可理解性。传统上两者紧密相连，因为数学家必须先 grasp 关键思想才能写出复杂证明。但AI可以生成形式化验证的证明，却未必提供可理解的论证。这种分离意味着，即使AI给出了逻辑上正确的答案，数学界也可能无法将其融入现有知识体系，从而无法推动数学进步。
数学不是有限游戏
文章反驳了将数学类比为象棋或围棋的观点。数学没有明确的胜负条件，也不是对抗性游戏。虽然数学家之间存在竞争，但数学的目标远不止解决问题，还包括发展理论、理解世界、培养社群等。因此，即使AI能解决所有问题，也不意味着数学被“解决”，因为数学的价值在于过程、理解和社群实践。
AI作为助手而非对手
文章引用Avigad的观点，认为应将AI视为服务人类目的的技术，而非与数学家竞争的对手。就像开车时不会与汽车比速度，使用手机时不会与手机比音量。真正的问题不是AI是否会击败数学家，而是我们希望AI服务于哪些数学目标。如果过于强调可基准化的解题能力，数学可能被AI同化，失去其人文和创造性维度。
Q&A
OpenAI 宣称用 AI 解决了纳维-斯托克斯问题，为什么作者认为这不算真正的数学解决？
作者指出，真正的数学解决需要同时满足逻辑正确和人类可理解两个层面的证明。OpenAI 提供的是形式化验证（Lean 证明）和一个看似对应的非形式化手稿，但数学界尚未确认它是否提供了可理解、能推进数学发展的证明。因此它只是一个“答案”，而非“解答”。
数学证明有哪两种概念？AI 的出现如何让它们分离？
文章区分了逻辑意义上的证明和可理解意义上的证明。逻辑证明关注演绎有效性，可由机械程序检验；可理解证明则要求数学家能 grasp、交流并用于进一步研究。传统上两者通常一起出现，因为数学家必须先理解关键思想才能写出复杂逻辑证明。但 AI 可以生成形式化证明却缺乏可理解性，导致两者戏剧性地分离。
为什么说数学不像国际象棋或围棋那样可以被 AI“解决”？
文章认为，国际象棋和围棋是有明确胜负条件的对抗性游戏，而数学没有类似的“将死”条件，也没有唯一的赢家。数学不仅仅是解题，还包括发展理论、理解世界、培养社群、创造美学价值等多元目标。因此，即使 AI 能解决数学问题，也不意味着数学被“解决”了。
如果未来 AI 能给出既逻辑正确又可理解的证明，数学是否就算被 AI 解决了？
作者认为仍然不算。因为数学的目标远不止解决问题，还包括发展新理论、统一不同领域、教育下一代、维持学术社群等。AI 可能打破“解决问题”与其他目标之间的正相关，所以即使 AI 能提供真正的证明，也不足以满足数学的全部追求。
作者建议数学家应该如何定位 AI 在数学中的角色？
作者建议将 AI 视为助手而非竞争对手。引用 Jeremy Avigad 的类比：我们开车时不会和车比谁快，用手机时不会和手机比谁声音大。数学家应思考希望 AI 服务于哪些数学目标，而不是担心被 AI 击败。
文章最后指出，AI 给数学带来的真正问题是什么？
真正的问题不是 AI 是否会击败数学家，而是我们希望 AI 服务于哪些数学目标。如果数学成功被过于紧密地等同于生产可验证的答案，数学可能会适应那些最容易被基准测试和自动化取代的特征。相反，如果数学家将 AI 视为推进数学长期人类目标的工具，它可能促进学科的繁荣。
