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

- 来源：Ethan Mollick (@emollick)
- 发布时间：2026-09-05 03:31
- AIHOT 分数：56
- AIHOT 链接：https://aihot.virxact.com/items/cmtndnmof04qvrog1bm5gpxjx
- 原文链接：https://x.com/emollick/status/2095957821644763561

## AI 摘要

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 的产出。仓库标注为研究产物，不维护且不接受贡献。

## 正文

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").

### 引用推文

> Lisan al Gaib：Anthropic just uploaded a Lean 4 proof for Fermat's last Theorem https://github.com/anthropics/fermats-last-theorem