AI开始"证明"数学了，数学家该慌吗？

你有多久没亲手验证过一个数学证明了？我最近看到Science上一篇关于AI驱动正式证明搜索的论文。形式化验证工具Lean、Coq折腾了好几年，但把AI真正嵌进去做证明搜索、还上了顶刊，这确实是头一回。有意思的是，数学界对AI的态度一直分裂。四色定理早交给计算机了，可"搜索新证明路径"这件事，直接挑战了人类最引以为傲的直觉。我的判断很明确：短期不替代，但会重塑分工。AI不会比顶尖数学家更聪明，但它不累、不偏颇、不会凌晨三点突然放弃。当它开始批量处理那些枯燥但必要的证明步骤时，人类创造力才有了真正触碰更深结构问题的空间。

原文：Advancing mathematics research with AI-driven formal proof search · 来源：Hacker News