计算机助力费马大定理形式化验证

费马大定理自1637年提出，历经358年才由怀尔斯完成首个完整证明。近期，伦敦帝国理工Kevin Buzzard教授领导团队利用Lean系统尝试将该证明形式化。过程中发现了关于晶体上同调的一个关键引理存在缺陷，但最终通过其他文献找到了替代证明方案。这一过程揭示了传统数学文献可能存在未被发现的问题，也展示了形式化验证的重要性。目前该项目已取得重要进展，有望为未来数学证明提供更可靠的保障。
来源：https://mp.weixin.qq.com/s/Kg22tpGacus09TNGuwkPkQ