Anthropic 在 GitHub 上开源了费马大定理的完整机器检查证明，基于 Lean 4.33.1 和 Mathlib，遵循 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles 的论证路线。该证明已通过 Lean 内核、独立内核 nanoda 及 comparator 的验证，并以 Apa
Anthropic 发布费马大定理 Lean 4 完整机器检查证明