AI 「獨自」解開 30 年前的數學難題

Harmonic 宣布，Aristotle「獨自」證明艾狄胥問題第 124 號（Erdos Problem #124），並用 Lean 4 語言完成了「形式化驗證」（Formal Verification）。 

這是懸宕近 30 年的數論猜想，這意味：證明是 100% 邏輯正確的，沒有模糊空間，沒有 AI 幻覺。未來數學研究，人類負責提供 "Vibe"（直覺與猜想），而 AI 負責處理繁瑣、艱深且需要絕對嚴謹的證明過程。 

未來在AI助威下，研究生一週讀一百篇論文是可能的。菜鳥瞄準一百篇的範圍後，擇優一週精讀一篇就很好了，上翻譯工具，語言憑障都消失了。讀書會和討論小組顯得更重要了，怎麼用人類精華的判斷力來辨認方向，集體智慧還是很有用的。