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 的产出。仓库标注为研究产物，不维护且不接受贡献。
Ethan Mollick@emollickAnthropic 在 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 的产出。仓库标注为研究产物，不维护且不接受贡献。
It is funny that the Fermat's Last Theorem proof description, short as it is, still smells so much of Claude ("names each step and the Lean Theorem that carries it").