Anthropic 上传基于 Lean 4 的费马大定理机器校验证明，Ethan Mollick 指出文档仍带有 Claude 文风

Anthropic 在 GitHub 上传了费马大定理的 Lean 4 完整机器校验证明（https://github.com/anthropics/fermats-last-theorem），基于 Mathlib（Lean 4.33.1、Mathlib v4.33.0），论证路线为 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles。Ethan Mollick 转发并评论称，该证明的描述虽短，但 PROOF-PATH.md 中"为每一步命名并标注对应 Lean 定理"的写法仍很像 Claude 的产出。仓库标注为研究产物，不维护且不接受贡献。