# Anthropic 开源 Lean 4 项目：把费马大定理的证明变成了机器能检查的代码

> 原标题：Fermat's Last Theorem in Lean 4

- 来源：Hacker News 首页
- 发布时间：2026-09-04T18:57:32.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/54833
- 原文：https://github.com/anthropics/fermats-last-theorem

## 摘要

Anthropic 开源了一个 Lean 4 项目，把费马大定理的证明翻译成了机器可验证的代码。费马大定理说的是 xⁿ + yⁿ = zⁿ 在 n>2 时没有正整数解，1994 年由 Wiles 证明。Lean 4 是一种证明助手，能把人的推理拆成一步步形式化步骤，让计算机逐条检查。这个项目是把已有的证明移植到 Lean 4，不是新定理。正文没披露花了...