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

野心的なオープンソースプロジェクトが、Lean定理証明器を用いてフェルマーの最終定理を形式的に証明することを目指しています。ケビン・バザードが主導し、EPSRCの資金提供を受け、インペリアル・カレッジ・ロンドンでホストされています。このプロジェクトでは、リチャード・テイラーとの協力の下、ウィルズ/テイラー・ウィルズによる元の証明の現代的な変種を採用しています。プロジェクトのウェブサイトでは、フェルマーの最終定理、Lean定理証明器、プロジェクトの目標、貢献ガイドラインに関する詳細情報を提供しています。