# Fermat's Last Theorem

A statement in qed.bot, the register of claims of AI work in mathematics. The register grades the evidence attached to each claim; it never rules on whether a proof is correct.

- Identifier: mathlib:FermatLastTheorem
- Collection: Mathlib
- Page: https://qed.bot/s/mathlib-fermatlasttheorem
- Formal record: unclassified; at its source: solved
- Machine-checked: no independent check has verified it
- Fidelity F2: The correspondence is declared through a Comparator challenge and written divergences.
- Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/FLT/Basic.html

## AI claims

### Claude, 4 Sep 2026

A complete Lean 4 proof of Fermat's Last Theorem on the standard axioms, deriving Mathlib's own statement, with the classical inputs proved in the strength the argument needs rather than assumed.

- Outcome: full (a supporting task)
- Autonomy A1: Collaborative. A human and a system worked the problem together, or the system played a supporting role.
- Evidence V2: Artifact reported. A proof or a constructed object is published, but nobody independent of its authors has rebuilt it.
- Fidelity F2: Declared. The authors record how the formal statement corresponds to the claim — a comparator challenge, an alignment table or written divergences — or a statement corpus cites the proof against its own statement.
- Source: Anthropic, Formalizing Fermat's Last Theorem, https://www.anthropic.com/research/formalizing-fermats-last-theorem
- Source: Lean formalisation, https://github.com/anthropics/fermats-last-theorem

Cite as: qed.bot, "Fermat's Last Theorem", https://qed.bot/s/mathlib-fermatlasttheorem, as of 30 Sep 2026. The register's data is published under CC BY 4.0: https://creativecommons.org/licenses/by/4.0/