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

Fermat's Last Theorem in Lean 4

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