有这样一个网站，它专注于数学研究和问题解答，特别是与著名数学家保罗・厄尔德什（Paul Erdős）相关的问题。
它就是 Erdős 问题网站。该网站收录了厄尔德什提出的各类数学问题，涵盖了许多不同领域，如数论、组合数学、图论等。研究人员、数学爱好者和学者们可以在这个平台上提出、讨论和解决这些问题。
如今，AI 的帮助已经变得常规化，比如「Erdős 问题 」：
图源：https://www.erdosproblems.com/367
11 月 20 日，独立研究者、数学家 Wouter van Doorn 提出了一个（人类生成的）对该问题第二部分的反例，依赖于他认为成立的一个同余恒等式，并且他「确信有人能够验证…… 确实成立」。
图源：https://www.erdosproblems.com/forum/thread/367-1766
几小时后，著名数学家陶哲轩将这个问题提交给了 Gemini 2.5 Deep Think。仅过了大约十分钟，Gemini 2.5 Deep Think 给出了该恒等式的完整证明，并确认了整个论证。该论证使用了一些 p-adic 代数数论，虽然这些工具对这个问题来说有些过于复杂。
图源：https://gemini.google.com/share/81a65aecfd70
接着，陶哲轩花了大约半小时将这个证明手动转换为一个更基础的证明，并发布在网站上，结果证明应该在「vibe formalizing」到 Lean 的范围之内，即经过适当的转化，这个证明是可以在 Lean 中被形式化和验证的。
在帮助论证后，Wouter van Doorn 对陶哲轩表示了感谢。
两天后，数学家 Boris Alexeev 使用 Harmonic 的 Aristotle 工具完成了该问题的 Lean 形式化，并手动形式化了最终的命题，以防止 AI 的滥用。这个过程花费了两到三小时，输出结果如下所示：
图源：https://borisalexeev.com/t/Erdos367.lean
