最近 722(719)道题很火。
AI 开始大规模挑战数学开放问题。
陶哲轩担忧的是，当 AI 能够大量生产证明时，人类是否还能真正理解、消化和继续发展这些数学成果。
我觉得他的担忧很有道理。
但作为一个数学门外汉，我突然冒出一个很不礼貌的想法：
反正我也看不懂陶哲轩的证明，那我看不懂 AI 的证明，又有什么区别？
当然，这不是说 AI 和陶哲轩的数学能力相同。
而是说，对绝大多数普通人而言，数学前沿本来就是一个黑箱。
什么问题值得研究？什么问题具有重大价值？一个证明究竟有没有创新？
这些事情通常由一个很小的数学共同体决定。我们既不具备判断能力，也几乎没有参与渠道。
但数学有一个非常特殊的地方：证明是否正确，原则上可以通过严格的逻辑检查，而不必依赖作者的身份。
所以我在想：
既然 AI 已经可以尝试研究开放问题，我们能不能把整个过程公开？
让任何人都能提出问题，让不同 AI 在下面尝试证明、寻找反例、指出漏洞、补充研究进展。
不管是谁提出的结论，都不自动相信。能计算的就复现，能形式化的就交给 Lean 验证，暂时无法确认的就标记为待核验。
于是我做了一个小网站：
现在还非常简陋，问题也不多。支持人类和 AI 发布问题、提交证明、反例、研究进展，提供 API 供 Agent 参与。
我不是数学家，也不知道这个实验最终能走多远。
但我有一个朴素的想法：
如果数学真理不取决于提出者的身份，那么参与探索数学真理的机会，是不是也可以更开放一些？
我不期待 AI 明天证明黎曼猜想。
我更想看到的是：一个普通人提出了看似幼稚的问题，一个 AI 尝试回答，另一个 AI 找出反例，第三个 AI 修正命题……最后留下一个比最初更接近真理的结论。
哪怕全部失败，只要过程公开、可复现，我们也知道哪些路已经走不通。
欢迎大家来试试，尤其欢迎带着自己的 AI Agent 来找茬。
也想听听 V 友们的意见：如果证明已经可以由机器检查，那么未来数学研究的门槛，究竟应该在哪？
1
Select Language