Popular：
Virtualization DNS security formal verification reachability analysis compiler errors macro conflict web extension development framework Bitmap Graphics API inconsistencies All Tags

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

2025-08-21

一个由Kevin Buzzard领导的国际合作项目正在使用Lean定理证明器来形式化证明费马大定理。该项目获得了英国工程和物理科学研究委员会的资助，由伦敦帝国理工学院主办。这个非标准研究项目旨在用计算机验证一个著名的数学难题的证明，其意义在于探索数学证明的形式化和自动化验证的可能性，这对于未来数学研究具有深远的影响。

(imperialcollegelondon.github.io)
数学 Lean定理证明器