天津
来源：市场资讯
（来源：机器之心）
有这样一个网站，它专注于数学研究和问题解答，特别是与著名数学家保罗・厄尔德什（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 工具在数学领域的应用，其参与的研究或亲自上手的数学证明包括如下：
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
