Rendered from ATTRIBUTION.md at the root of the repository.

ATTRIBUTION — third-party material in this repository, file by file

This file accompanies NOTICE. It lists every file of this repository that we have identified as containing Lean text taken or adapted from a third-party project (106 files with material from the Imperial College London FLT project or the flt-regular project, §§1–3: 54 under Definitions/, 52 under P2M/Sol/; and the 23 files that reproduce Mathlib text, §4), names the upstream file(s), and reproduces the upstream copyright holder and author list. The Lean files are published byte-for-byte as they were checked and carry no attribution headers, apart from five files that retained an upstream notice in place (marked below) and the Mathlib provenance header of Definitions/Def_Compat_Mathlib430.lean (§4); for all the others this table is where the per-file notices are reproduced. Everything listed is licensed upstream under the Apache License, Version 2.0, the licence of this repository.

How this table was made

The Lean files of this repository were assembled by AI agents and were published without their comments, so upstream headers did not survive in place. To restore the attribution we compared, line by line after normalising whitespace and dropping import/open/namespace/section lines, every one of the 60,478 .lean files of the tree as it then stood on Lean 4.30.0 (its 60,474 modules, lakefile.lean and three Lean files under verification/, of which this release keeps two) against the copies of Imperial College London FLT files that had been brought into our working tree in May 2026 with their original headers intact (97 files from the upstream main branch as of 2026-05-21, plus three files of ours that were themselves ports of the upstream Frey-package and torsion files), and we cross-checked the result against the provenance notes that the files carried before their comments were removed (two files were ported directly from upstream commit 8387d589 of 2026-05-27 and are identified from those notes). A file is listed when it shares with an upstream file at least five distinctive lines (lines of 20 or more characters that occur in at most three upstream files and at most twelve files of this repository), or at least three such lines covering at least half of the upstream file; a few shorter passages found on review are listed too. "Extent" is the share of the file's non-blank code lines found in the named upstream file(s); it is approximate, and where a file lists several upstream files some of the matched lines are common to those files. The flt-regular rows rest on the pre-publication provenance notes alone (we had no copy of that project to compare against). The files published here are the port of that tree to Lean 4.33.1 and Mathlib v4.33.0: the port renamed Mathlib lemmas and adjusted proofs mechanically in 65 of the 106 listed files (under a tenth of the lines of each, except the 31-line Definitions/Def_Mathlib_RingTheory_DedekindDomain_AdicValuation.lean) and left the other 41 byte-identical, so the extents below, computed on the Lean 4.30.0 text, remain approximately right; which files are listed is unaffected. Limits of the method are stated in §5.

1. Files containing material from the Imperial College London FLT project

Upstream: https://github.com/ImperialCollegeLondon/FLT, branch main as of 2026-05-21 (the date our copies were taken; we did not record the commit hash) unless a commit is given. 90 files. Upstream paths are relative to that repository.

2. Files containing Imperial College London FLT material through an intermediate port

In May 2026 we ported the upstream Frey-package file and the torsion Galois-module file by hand into our working tree, restructuring them and adding material of our own; the files below contain text from those two ports (extents count only lines traceable to them, as best we can tell). The upstream paths and author lists given here are as recorded in our port's notes and have not been re-checked against the upstream repository, whose file headers are authoritative, with one exception: the notice of FLT/EllipticCurve/Torsion.lean below is the upstream file's own, at the commit named. 14 files.

3. Files containing material from the flt-regular project

Upstream: https://github.com/leanprover-community/flt-regular — A complete formalization of Fermat's Last Theorem for regular primes in Lean, Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Ruben Van de Velde, Andrew Yang (arXiv:2410.01466). Apache License, Version 2.0. That project's per-file headers are not reproduced in this revision; the project, its authors and the files drawn on are named instead.

4. Mathlib

This repository is built on Mathlib (https://github.com/leanprover-community/mathlib4, Apache-2.0, copyright the Mathlib authors as recorded in its file headers), which is fetched at build time and not distributed here. The Definitions/Def_Mathlib_* files listed in §1 are the Imperial College London project's "FLT/Mathlib" staging files, not copies of Mathlib files. Mathlib text nevertheless occurs in the tree in two ways.

First, one file copies Mathlib text wholesale. Definitions/Def_Compat_Mathlib430.lean reproduces, under new names and without their docstrings, the Mathlib v4.30.0 (commit c5ea00351c28e24afc9f0f84379aa41082b1188f) text of a few definitions, lemmas and one notation whose form changed in Mathlib v4.33.0 — verbatim apart from four lines marked -- [port] — each copied block headed by the Mathlib file and line range it is taken from; it also contains two small bridging declarations of our own (Representation.ofMulActionFinsuppEquiv, Rep.ofMulActionFinsuppIso), three one-line example checks and, in its last block, four lemmas adapted and re-proved from Mathlib/NumberTheory/RamificationInertia/Galois.lean rather than copied. The eight Mathlib files it draws on and their notices (identical at Mathlib v4.30.0 and v4.33.0; each header, here and in the second table, continues "All rights reserved. Released under Apache 2.0 license as described in the file LICENSE.") are listed in the first table below.

Second, some modules re-prove a Mathlib lemma in place — usually a private or auxiliary Mathlib result the module needed — and in doing so reproduce its proof text. To find these we compared every .lean file of this repository, line by line after normalising whitespace and dropping import/open/namespace/section lines, against every file of Mathlib v4.33.0 (commit db584cd6d46c92f209a44c0f1c829460d327499d) and v4.30.0, and list below the modules this comparison identified as sharing a run of roughly eight or more consecutive lines with a Mathlib file, setting aside matches that are only routine structure-instance boilerplate. Twenty-two modules are listed (twenty-one under P2M/Sol/, one under Definitions/; one of them, P2M/Sol/S_flt_regular.lean, also appears in §3 for its flt-regular material); the second table below gives for each the Mathlib file, that file's copyright holder and authors (verbatim from its header), what was taken, and the approximate extent. The comparison is sensitive to how lines are normalised; shorter restatements, and proofs that follow a Mathlib argument without reproducing its text, are not listed individually; Mathlib as a whole is credited in NOTICE.

5. What we are not certain of

• Coverage. The comparison corpus was the set of upstream files present in our working tree (100 files). Upstream files that were never copied into our tree cannot be detected by this method; for those we relied on the pre-publication provenance notes, which name no further Imperial College London or flt-regular files beyond those listed. If further material is recognised, the omission is ours and unintentional.
• Two headers supplied from upstream. Definitions/Def_DedekindDomain_Completion_BaseChange.lean and Definitions/Def_DedekindDomain_FiniteAdeleRing_BaseChange.lean are ports of FLT/DedekindDomain/Completion/BaseChange.lean and FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean at upstream commit 8387d589441c1097d606ea89370c4165147255d5; our copies did not retain those two files' notices, so the copyright and author lines given for them in §1 were read from the upstream files at that commit and are reproduced here.
• Upstream revision. Our copies record the upstream branch (main) and the date (2026-05-21), not a commit hash; one file (FLT/EllipticCurve/Torsion.lean) was recorded at commit 7a87d3b25db19d008cd45b29edd2b92803e785b1, two at 8387d589… as above.
• §2 paths and author lists come from our own May porting notes ("FLT/Basic/FreyPackage.lean … Kevin Buzzard, Ruben Van de Velde, Pietro Monticone"; "FLT/EllipticCurve/Torsion.lean"), as does the notice retained in Definitions/Def_FLTPrelim_FreyPackage.lean; apart from the notice of FLT/EllipticCurve/Torsion.lean, read from the upstream file at commit 7a87d3b25db19d008cd45b29edd2b92803e785b1 and reproduced in §2, none has been re-checked against the upstream repository.
• flt-regular per-file headers are not reproduced in this revision; §3 names the project and its authors instead.
• Small passages. Below the thresholds above (a handful of shared lines) we did not attribute systematically; such passages are typically routine instance declarations or one-line lemmas. A few found on review are listed.