Learning source excerpts preserve the original files and their headers. FLT source: anthropics/fermats-last-theorem, Apache-2.0; see ../LICENSE, ../NOTICE and ../ATTRIBUTION.md. Additional Mathlib files: leanprover-community/mathlib4, Apache-2.0; see mathlib/LICENSE. The Mathlib revision is the one selected by the pinned FLT lake-manifest.json. Editorial explanations belong to Fun Lean and are not formal proof statements.