机器之心报道
机器之心编辑部
有这样一个网站，它专注于数学研究和问题解答，特别是与著名数学家保罗・厄尔德什（Paul Erdős）相关的问题。
它就是 Erdős 问题网站。该网站收录了厄尔德什提出的各类数学问题，涵盖了许多不同领域，如数论、组合数学、图论等。研究人员、数学爱好者和学者们可以在这个平台上提出、讨论和解决这些问题。
如今，AI 的帮助已经变得常规化，比如「Erdős 问题 #367」：
11 月 20 日，独立研究者、数学家 Wouter van Doorn 提出了一个（人类生成的）对该问题第二部分的反例，依赖于他认为成立的一个同余恒等式，并且他「确信有人能够验证…… 确实成立」。
几小时后，著名数学家陶哲轩将这个问题提交给了 Gemini 2.5 Deep Think。仅过了大约十分钟，Gemini 2.5 Deep Think 给出了该恒等式的完整证明，并确认了整个论证。该论证使用了一些 p-adic 代数数论，虽然这些工具对这个问题来说有些过于复杂。
接着，陶哲轩花了大约半小时将这个证明手动转换为一个更基础的证明，并发布在网站上，结果证明应该在「vibe formalizing」到 Lean 的范围之内，即经过适当的转化，这个证明是可以在 Lean 中被形式化和验证的。
在帮助论证后，Wouter van Doorn 对陶哲轩表示了感谢。
两天后，数学家 Boris Alexeev 使用 Harmonic 的 Aristotle 工具完成了该问题的 Lean 形式化，并手动形式化了最终的命题，以防止 AI 的滥用。这个过程花费了两到三小时，输出结果如下所示：
近年来，陶哲轩一直持续探索 AI 工具在数学领域的应用，其参与的研究或亲自上手的数学证明包括如下：
谷歌 AlphaEvolve 太香了，陶哲轩甚至发了篇论文，启发数学新构造
陶哲轩：用了 GPT-5 Pro 后，小尺度、宏观尺度很赞，中尺度有点垮
陶哲轩：感谢 Lean，我又重写了 20 年前经典教材！
刚刚，DeepMind 通用科学智能体 AlphaEvolve 突破数学极限，陶哲轩合作参与
陶哲轩：感谢 ChatGPT，4 小时独立完成了一个开源项目
……