Technical Lean evidence record
Checked Artifact: Fermat's Little Theorem (mathlib)
Proof Atlas collected build, no-sorry, axiom, and clean-source evidence directly from the pinned upstream declaration.
Four separate status axes
Upstream indexedPinned source bytes verified locally
Locally reproducedExact upstream declaration replayed
Reviewed page2 of 3 presentation reviews recorded
Accepted Atlas resultNot recorded for the preferred artifact
These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.
Mechanical evidence
- Declaration checked
Nat.ModEq.pow_card_sub_one_eq_one- Module
Mathlib.FieldTheory.Finite.Basic- Source file checked
Mathlib/FieldTheory/Finite/Basic.lean- Package commit
5e932f97dd25535344f80f9dd8da3aab83df0fe6- Build
- passed · transcript retained
- Unfinished proof steps
- None found by the recorded no-sorry scan
- Axiom closure
- Classical.choice, Quot.sound, propext
- Clean collection provenance
- Recorded
Evidence boundary
This target indexes Mathlib's natural-number congruence form: if p is prime and n is coprime to p, then n^(p-1) is congruent to 1 modulo p. It does not state the alternate n^p congruent to n form, primality converses, or a new proof.
This checker record is evidence for the exact formal statement only. It does not establish novelty, transfer a historical acceptance decision, or authorize publication.