最近 722(719)道题很火。 AI 开始大规模挑战数学开放问题。 陶哲轩担忧的是，当 AI 能够大量生产证明时，人类是否还能真正理解、消化和继续发展这些数学成果。 我觉得他的担忧很有道理。 但作为一个数学门外汉，我突然冒出一个很不礼貌的想法： 反正我也看不懂陶哲轩的证明，那我看不懂 AI 的证明，又有什么区别？ 当然，这不是说 AI 和陶哲轩的数学能力相同。 而是说，对绝大多数普通人而言，数学前沿本来就是一个黑箱。 什么问题值得研究？什么问题具有重大价值？一个证明究竟有没有创新？ 这些事情通常由一个很小的数学共同体决定。我们既不具备判断能力，也几乎没有参与渠道。 但数学有一个非常特殊的地方： 证明是否正确，原则上可以通过严格的逻辑检查，而不必依赖作者的身份。 所以我在想： 既然 AI 已经可以尝试研究开放问题，我们能不能把整个过程公开？ 让任何人都能提出问题，让不同 AI 在下面尝试证明、寻找反例、指出漏洞、补充研究进展。 不管是谁提出的结论，都不自动相信。能计算的就复现，能形式化的就交给 Lean 验证，暂时无法确认的...