有這樣一個網站，它專注于數學研究和問題解答，特別是與著名數學家保羅?厄爾德什（Paul Erd?s）相關的問題。

它就是 Erd?s 問題網站。該網站收錄了厄爾德什提出的各類數學問題，涵蓋了許多不同領域，如數論、組合數學、圖論等。研究人員、數學愛好者和學者們可以在這個平臺上提出、討論和解決這些問題。

如今，AI 的幫助已經變得常規化，比如「Erd?s 問題 #367」：

圖源：https://www.erdosproblems.com/367

11 月 20 日，獨立研究者、數學家 Wouter van Doorn 提出了一個（人類生成的）對該問題第二部分的反例，依賴于他認為成立的一個同余恒等式，并且他「確信有人能夠驗證…… 確實成立」。

圖源：https://www.erdosproblems.com/forum/thread/367#post-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