A "proof" of Fermat's Last Theorem that fits the margin
21 days ago
- 费马声称证明了费马大定理，但因边页空白太少而未写出证明。
- Anthropic 用1300万行Lean代码形式化了费马大定理。
- Lean的 String.Pos.Raw.extract 中存在一个bug，导致不匹配：逻辑评估返回空字符串，而原生评估返回完整字符串。
- 这一矛盾允许在Lean中证明任何命题，包括费马大定理。
- Lean团队迅速修复了该bug：约90分钟内完成了内存安全修复，5天内修复了语义不匹配。
- 额外公理 native_decide 将编译器加入可信边界，需谨慎使用。
- 需要更多工作（例如 lean4lean、替代内核）来确保证明的正确性，以防止此类利用。