陶哲轩谈数学研究：AI 自动证明加速下好问题可能成为被采空的资源

陶哲轩指出纯数学中的开放问题正在成为被开采的不可再生资源，如果借助自动化工具开采得过于粗糙，数学研究获得的净收益反而会减少。他以等式理论项目在 Lean 中形式化解决 2,200 多万个泛代数蕴涵关系为例，说明部分难题曾逼出构造无限反例的新技术，若自动定理证明器提前找出极小的有限反例，更有价值的数学方法可能就不会出现。