陶哲轩：好问题是会被采空的资源

陶哲轩以参与的等式理论项目（ETP）为例指出，该项目用几个月解决了 2,200 多万个泛代数蕴涵关系并在 Lean 里形式化，其中几处蕴涵曾逼出构造无限反例的新技术，后来自动定理证明器却发现它们其实有很小的有限反例。他认为数学史上第一次，纯数学里的开放问题被当成不可再生资源来开采，开采得粗糙，数学得到的净收益会少得多。