陶哲轩的“数学2.0”愿景与AI证明警告

陶哲轩的《数学2.0》一文指出，数学的核心制度——终身教职、奖项、期刊发表以及率先攻克著名未解难题的声望——都是建立在“证明稀缺”这一假设之上的，即解决难题象征着罕见的人类专长^[1]。他对变化的描述直截了当：“我们将从证明稀缺的时代过渡到证明丰裕的时代”^[2]。这种转变破坏了该领域的隐性激励结构，因为问题求解从来就不应是数学的最终目标——它只是理解的代理。陶哲轩最尖锐的一句话直接点明了这一点：“继续单纯盲目地优化问题求解，现在已对数学的长期健康构成实质性危害”^[3]。一旦AI能够廉价且大规模地生成证明，一个仍以解题数量为奖励标准的领域就是在优化错误的指标——它生产了更多答案，而这些答案本应体现的人类洞察力却未被检验和培养。

陶哲轩创造了“证明消化不良”一词，用以描述AI生成的定理通过形式化Lean验证的速度快于人类解释、教学或吸收它们的场景——他指出，“海量的机器生成定理通过了Lean验证，但即便是启动这些运行的工程师也无法解释其背后的机制”^[4]。他将此与另一个相关担忧联系起来：他将未解难题比作“灯塔”，其价值不在于作为目的地，而在于引导探索周边的数学景观。他认为，数学家在尝试解决难题过程中所学到的东西——失败的方法、新技术、沿途绘制的周边领域——往往比最终答案更有价值^[5]。一个在不产生任何周边洞见的情况下直达终点的AI系统，不仅未能提供帮助；在陶哲轩看来，它还可能“使问题周边环境变得贫瘠”，摧毁了未来数年人类探索工作的动机，而这些探索本应围绕该问题持续展开。

陶哲轩的文章并非凭空出现。几天前，OpenAI发布了700多份手稿（其他报道称为370多个已解决的问题），声称解决了大量数学未解难题，包括在千禧年大奖难题上的部分进展，平均每项解决方案耗时约三小时计算资源^[7]。这一发布引发了数学家的“震惊与厌恶”反应，包括菲尔兹奖得主雨果·杜米尼尔-科潘所言：“震惊是巨大的。我完全瘫痪了。”同时引发疑问：“我们失去了多少美感？”^[8]。在发布之前，反弹情绪已在酝酿：25位菲尔兹奖得主，包括陶哲轩和彼得·朔尔策，已共同签署了一份9月11日的声明《人工智能与数学的严重错位》，警告AI公司的商业激励——速度、基准宣称、宣传——与数学界缓慢、基于验证、重视归属的文化相冲突^[9]。人类数学协会更进一步，呼吁抵制，并将此次发布描述为“不是学术的展示，而是权力的展示”。陶哲轩的《数学2.0》框架可视为同一反应的建设性一面——与其说是对OpenAI的直接攻击，不如说是试图设计出能够抵御此类事件再次发生的激励结构。

陶哲轩的答案并非停止AI辅助数学，而是重新设计该领域所奖励的内容。通过他共同创立的非营利组织SAIR，他推动了“开放数学模型”倡议，提供透明、可检查的模型权重，以抗衡封闭的前沿系统^[10]。此外，他的数学2.0提议包括“开放阐述问题”，奖励清晰解释而非优先求解；动态的研究成果网络；大型形式化库（如Mathlib）；以及测试定理证明实际鲁棒性的消融研究——所有这些都旨在将领域的激励重新导向理解，而非解题数量。陶哲轩坦率地指出了障碍：“实现数学2.0的主要瓶颈不是技术……而是想象力”^[6]。然而，如果一家AI实验室根本没有理由采纳数学界为自己建立的以阐述为导向的规范，这一切都无法解决随之而来的问题。

并非所有数学家都以相同方式解读陶哲轩的警告。多伦多大学数学家丹·利特对OpenAI的发布持相反观点，称这波AI生成的解决方案“对数学大有裨益”^[7]——这与朔尔策坚持“目标始终是人类对数学的理解”形成直接对立^[8]。这种分歧大致反映了学界对数学2.0的更广泛分歧：一派将陶哲轩等人的担忧视为可以理解但最终是既得利益领域抗拒自动化的防御；另一派则将其视为一个具体而狭隘的教学论点——即瞬间解决问题剥夺了下一代数学家尝试难题的训练场。陶哲轩本人试图将分歧提升一个层次，将学界的危机定义为价值观问题而非能力问题，并呼吁数学家集体回应：“我们必须组织起来，成为行动者，变得有点政治化”^[6]。尚未解决的紧张关系在于，陶哲轩所押注的激励机制重构，是否真能与驱动AI实验室发布此类成果的速度和宣传激励相抗衡。