AIが数学者の反例探しを追い抜く：Grothendieck予想への反例がLeanで検証される

Human mathematicians are being outcounterexampled

数学の自動形式化とAIツールの進展により、数学者がAIによって反例を見つけられる時代が到来した。本稿では、Erdősの単位距離予想の反例がChatGPTによって発見され、Logical IntelligenceとOpenAIのSolがそれをLeanで形式化した事例、さらにGrothendieckの群スキームに関する60年来の未解決問題に対する反例がSolとFableによって発見され、Leanで検証された事例を紹介する。また、Jacobian予想への反例も報告され、AIが数学研究の最前線で重要な役割を果たしつつあることを示す。著者は、AI生成の数学を信頼するには形式化が不可欠だと強調する。