Anthropic使用其内部模型在prove2.me平台上用Lean形式化了费马大定理的完整证明，这是Freek Wiedijk著名100个形式化挑战列表中最后一个被形式化的定理，标志着历时20年的里程碑项目正式完成。该证明基于Darmon-Diamond-Taylor对怀尔斯-泰勒-怀尔斯论证的阐述，代码量超过1340万行。
背景
Freek Wiedijk的100个形式化挑战列表自21世纪初以来一直是形式化数学社区的基准测试，费马大定理是其中最难的未解决问题之一。Xena项目一直在致力于用Lean形式化FLT，作为其通过数学实践教授Lean的教育使命的一部分。
- 来源
- Lobsters
- 发布时间
- 2026年9月5日 03:11
- 评分
- 9.0 / 10