“Math 2.0” 将需要更全面地衡量数学进步的价值
AI 生成的数学证明正在快速进展，迫使数学界重新思考什么才算真正的进步：仅仅是解决开放问题，还是发展人类理解、优雅方法和新的研究方向。许多人认为，大量投放由机器生成、往往以 Lean 等系统形式化但难以解读的证明，会让问题“被污染”，削弱动机，并破坏学术界既有的激励结构；而另一些人则认为，这只是自动化的自然且有价值的延伸。围绕这场争论，还浮现出一个对许多职业都适用的更广泛问题：在前沿结果可能由解决问题能力超人的系统产出、却尚未擅长解释或传递洞见的时代，教育、职业和署名/归功机制该如何重设计。
数学的目的与证明的价值
- 许多人认为，数学关乎理解、洞见和新工具，而不只是拥有一个正确的证明。
- AI 生成的 Lean 证明虽然能“解决”问题，但往往缺乏清晰的概念性收获、优雅的结构，或可复用的方法。
- 也有人反驳说，一个正确的形式化证明本身就是永久性的贡献；之后的简化与解释仍然可以由人类（或未来的 AI）来完成。
AI 证明对数学生态系统的影响
- 当前的奖励结构重视率先解决著名开放问题；AI 的“大规模抢跑”打破了这一模式，可能会打击人类的研究积极性。
- 有人担心问题已经被“污染”：一旦存在 AI 解决方案，人类主导的替代证明或洞见就会被低估并缺乏资助。
- 还有人担心，成百上千篇密集、半可读的 AI 论文把“苦活”（验证、阐释、整合）转嫁给一个回报不足的社区。
当前 LLM 的能力与局限
- 支持者认为：模型已经能够产出形式化、可验证的证明，而且大概率会在解释、简化和探索方面继续进步；幻觉和粗糙被视为工程问题。
- 怀疑者认为：模型更擅长追求正确性而非优雅，往往依赖带有繁复构造的蛮力方法，并且在教学和“品味”方面表现薄弱。
- 讨论的焦点之一是：LLM 能否真正原创出新的抽象，还是只能以巨大的规模重组已有思想。
激励机制、职业与资金
- 人们普遍担忧数学职业，尤其是纯数学，会缩减，或转向教学、阐释、验证或应用工作。
- 也有人认为，当前公共资助本就已经扭曲——“定理经济”和声望竞赛——AI 只是暴露了长期存在的问题，而不是制造了这些问题。
- 另一些人强调“无用”数学在长期中的价值，并为以好奇心驱动的研究辩护，认为这是一种正当的公共利益。
与其他领域和自动化的比较
- 类比包括国际象棋/围棋（企业实验室证明某事后便转身离开，由社群接手）、软件工程（AI 作为强大但凌乱的协作者），以及工艺/体育（人类实践仍作为艺术/爱好而延续）。
- 有人推测，数学将分化为：完全人类的“艺术数学”、人机混合研究，以及完全自动化的前沿工作。
拟议回应与开放问题
- 有人呼吁将价值评估转向阐释、社区建设、新方向，以及对 AI 结果的整合。
- 也有人建议把结果表述为“存在一个 Lean 证明”，而不是“问题已被解决”。
- 仍不清楚的是：如何设计新的激励机制，前沿上什么仍然是人类独有的，以及未来模型是否会让深层的人类级解释变得平凡，还是会进一步扩大差距。