Leanを用いたフェルマーの最終定理の形式化：協調的なオープンソースプロジェクト

ケビン・バザード率いる国際的な協力プロジェクトは、Lean定理証明器を用いてフェルマーの最終定理を形式的に証明するという野心的な取り組みを行っています。英国工学物理科学研究会議の助成金を受けており、インペリアル・カレッジ・ロンドンを拠点としています。このプロジェクトは、コンピュータによる証明検証を通じて、数学における形式化と自動検証の可能性を探求し、将来の研究に影響を与えます。