用Lean证明费马大定理：一个雄心勃勃的开源项目

一个名为Lean的开源项目正在尝试用形式化方法证明费马大定理。该项目由Kevin Buzzard领导，得到了英国工程与物理科学研究委员会（EPSRC）的资助，并由帝国理工学院提供支持。项目计划采用Wiles/Taylor-Wiles证明的现代变体，路线图由Richard Taylor和Buzzard共同制定。项目页面提供了关于费马大定理、Lean证明器以及项目目标的更多信息，并欢迎大家的贡献。