陶哲軒によるAIを用いた多項式Freiman-Ruzsa予想の証明

陶哲軒氏がAIツールを用いて多項式Freiman-Ruzsa予想の証明を形式化したことが、数学界に大きな衝撃を与えています。これは、数学研究における人工知能の広範な応用を示す画期的な出来事です。

氏は自身のブログで、Lean4を用いてBlueprintで証明を形式化する過程を詳しく記述しています。このプロジェクトは3週間で完了し、多項式Freiman-Ruzsa予想の証明の形式化に成功しました。人工知能が数学研究において発揮する驚異的な力を示す成果と言えるでしょう。