Interactive apps
- Play — the worksheet reader new — the
lean/play/worksheets in the browser, without an IDE or a Lean install: zones and prose, and a card for every checked declaration with its sugared source, docstring, module and one layer of references. Replaces the#check/#print/ go-to-definition loop for reading.
Open Play →
Published copy: htzh.github.io/flt_for_human/play; in a clone, build it first. - Modularity, computed — a Weierstrass-equation workbench: minimal
model, discriminant, conductor, traces of Frobenius by point counting, and the
weight-2 eigenform
q-expansion reconstructed from the Hecke recursions. Companion to note 007.
Open the app →
Lean porting effort
Alongside the prose, this project re-runs selected pieces of the FLT formalisation as our own Lean code. A claim that matters can then be checked rather than taken on faith, and a proof can be restated in a form we find easier to read.
- 621 Lean modules under
lean/FLTForHuman/ - Lean v4.34.0 · mathlib v4.34.0
- Fragments only — mathlib is the sole import
- Every module cites its FLT origin pinned at
aa2d8b3
The ground rules: copy small, self-contained definitions and lemmas out of
FLT and adapt them — never import the FLT project (one import can pull in a
dependency cone and a build measured in hours); adapt rather than mirror, since FLT stays
the source of truth for correctness; cite the origin file and commit in each module header;
and leave no silent gaps — a module either compiles or carries an explicit, commented
sorry.
- lean/README.md — how the port is organised, pinned, and built.
- Porting playbook — the reusable method for porting a node, not tied to any one effort.
- FLTForHuman/ — the verified tree: the ported fragments, by subject.
- topics/
— work orders and executed plans (
PORTING-*.md) for each effort, with what it cost and what it taught. - spec/ — the deliverable measures: consumer modules, the statement checker, and the register of the unwired public surface (generated locally; not committed).
- Carry-forward register — API deliberately left unported, and the open follow-ups.
- logs/ — the linear record of what happened, in order.
▶ Math notes 27 one step of the FLT proof, opened up · newest first · click a group to expand
This revision adds notes 013, 015–022 and 024–027.
Browse math/ on GitHub ↗
▶ Frontier: level structure and the adelic turn 024–027
- 027 — The continuity of the idele norm
new
the idele norm, and the norm of the determinant onGL₂over the adeles, are continuous in the restricted-product topology — the two most heavily depended-on theorems of the pin'sNumberField.TateGloballayer - 026 — ℘-division values and the level-N modular curve
new
Fricke functions turn torsion values of ℘ into weight-zero modular functions: SL₂(ℤ) permutes them, the tuple is fixed exactly by ±Γ(N), ℂ(X(N)) = ℂ(j, f_v) is Galois of degree the index, and Shimura's reciprocity law acts on the q-expansions of Δf_v - 025 — Elliptic nets, division polynomials, and the invariant of a sequence
new
the classical [n]P formula assembled from three layers — ψ_n as the canonical normalised elliptic divisibility sequence, the elliptic-net relation behind every ψ identity, the complement that avoids ψ₂ₙ/ψ_n, and the invariant 6X²+b₂X+b₄ that removes the division by y, so the construction survives every characteristic - 024 — Uniformization and the modular function field: two routes to the j-line
new
the ℚ(j(q), j(qᴺ)) function field and the analytic ℂ/Λ ≅ E(ℂ) theory are complementary, not interchangeable — two independent inputs to the same step of Mazur's irreducibility argument, and the uniformization's surjectivity of j is itself proved by modular forms
▶ Residues, Deligne–Serre, and the T side of R = T 018–023
- 023 — Vélu isogenies, the quotient j-invariant, and the endomorphism ring
isogenies as function-field extensions: Vélu's explicit formulas and the quotient j, the modular polynomial Φ_N as the cyclic-quotient correspondence, dual/trace/norm of the endomorphism ring, the CM dichotomy, and the two chains by which all of it reachesfermat_last_theorem - 022 — The global residue theorem over an algebraically closed field
residueTheoremK_of_isAlgClosed: the residues of a meromorphic differential over an arbitrary algebraically closed field sum to zero — the algebraic replacement for the analytic theorem, built on the Tate residue of 021 - 021 — The Tate residue, and the agreement theorem
Tate's commutator definition of the residue over a field that is not ℂ, andtateAgreementidentifying its trace with the trace of the classical local residue - 020 — Frobenius elements, Chebotarev density, and finite-image Galois representations
the Frobenius-at-a-place vocabulary, the density theorem governing it, and the two representation-theoretic consequences the Deligne–Serre argument needs - 019 — Deligne–Serre for weight one: odd Artin representations
the weight-one correspondence and where it sits among the modularity theorems the FLT development uses - 018 — The T side of R = T: the definition layer
the mathematics of the T-side definitions, in the order the Lean import closure forces
▶ Hecke, Eichler–Shimura, and the integral structure 013–017
- 017 — The Eichler–Shimura isomorphism
the classical isomorphism and the constructions it rests on; the Lean inventory and the port plan live in the scout and topic files - 016 — The mod-p weight filtration, and the gap in the Eichler–Shimura cohomology-packaging bypass
the open “gap” that decides whether the analytic Eichler–Shimura period map can be dropped from the endgame — its mathematics, and the routes around it - 015 — Finiteness of the weight-two Hecke algebra from periods
why the weight-two Hecke algebra is finite, proved on its own from periods in the pin's 4,308-line route-B file — the counterpart of the integral-structure route - 014 — The χ₋₃ weight-one Eisenstein series and the hexagonal lattice
r(n) = 6σ_χ(n): the hexagonal form as the norm of ℤ[ζ₆], the six units, the ramified/split/inert laws, Poisson summation and the Fricke equation, and why the mod-3 congruence powers the weight-two lift - 013 — The integral structure of cusp forms from an integral Γ₁-basis
the ℤ-span of the cusp forms with integral q-expansion is full-rank in S_k(Γ₀(N)) — an integral ℂ-basis exists
▶ Modularity, the Tate module, and the level theory 009–012
- 012 — The Sturm bound
a modular form is determined by ≈ k/12 · [SL₂(ℤ):Γ] coefficients; level one from the dimension formula, arithmetic level by the norm, and how the bound makes the integral lattice finitely generated - 011 — The Tate module and the attached Galois representations
T_pE = lim E[pⁿ] and its rank two, the Galois action and its adic continuity, det ρ = χ, Frobenius and point counts, stable lines as isogenies, and the Eichler–Shimura side: T_pJ₀(N), Hecke eigenforms and ρ_f - 010 — Function field generation for X₀(N)
the modular equation Φₚ and its root slots, descent by one prime, the prime-power degree steps, and the strong induction proving ℚ(j, j(qᴺ)) = ℚ(j(qᵈ) : d | N) - 009 — The Hecke action on the Jacobian, and why it commutes
X₀(N) as a function field inside ℚ((q)), J₀(N) = Pic⁰, T_ℓ = α_*∘β^*, the exchange square, the modular equation
▶ The Frey route 001–008
- 008 — Ribet's level lowering in the FLT proof
squarefree conductor, v_q(Δ) = 2p, stripping one prime at a time, dim S₂(Γ₀(2)) = 0 - 007 — Modularity and computation
the modularity theorem, computed; companion to the app - 006 — Fixed or cofixed, and inertia
how the Frey curve's semistability splits every stable line, and why inertia decides - 005 — #E[n](K) = n² over an algebraically closed field
the fibre count of multiplication by n — the foundation of the GL₂ picture - 004 — Irreducibility and the cofixed line
how the mod-p representation is excluded without ever being named - 003 —
GaloisRepIsIrreducible, in English
and why the generalAffine Raccepts the Frey curve - 002 — The Frey curve: the E_p model vs. the original form
where the discriminant is computed - 001 — The Frey package and WLOG normalisation
why a Frey package is enough, WLOG, for every prime exponent p ≥ 5
▶ Base notes 22 the mathlib layers the proof is written against · grouped by subject, so order is not a path · click a group to expand
This revision adds notes 008–022.
Browse base/ on GitHub ↗
· reading order and background: base/README.md
▶ Latest additions 019–022
- 022 — Haar measure: invariance, unimodularity, and convolution on the adeles
new
left- versus right-invariance, Haar existence and uniqueness, the modular character, the stable-range proof that GL₂(𝔸_F) is unimodular, convolution as invariance plus Fubini, and the pushed-forward measure the automorphic right-convolution topic is written against - 021 — Uniformization: ℂ/Λ ≅ E(ℂ)
new
the purely complex-analytic proof that z ↦ (℘(z), ℘′(z)/2) is a surjective homomorphism with kernel Λ — the Weierstrass differential equation, Liouville, and the two addition laws - 020 — The index of Γ₀(N), and the two functions that count it
new
[SL₂(ℤ):Γ₀(N)] = ψ(N) through the coset bijection with ℙ¹ over ℤ/N, and #primCosetReps(N) = ψ(N) through an independent explicit count; Euler's φ beside Dedekind's ψ, and what is mathlib's and what is ours - 019 — Stichtenoth's genus and the adelic index
new
the adelic engine that manufactures the genus and Riemann–Roch without analysis or differentials — bounded adeles, the index of speciality, the bounded defect, Stichtenoth's pole-divisor bound, and Weil differentials; the fourteen declarations of the phase-1 RR port
▶ Curves: divisors, places, and Riemann–Roch 008–010 · 015–017
- 017 — The rational function field and principal divisors
deg div(f) = 0 proved on K(t) by unique factorization and transferred to a general function field by the norm and pushforward - 016 — Correspondences and the exchange lemma
pull–push as ψ_*∘φ^*, the fibre-square exchange identity, its reduction to a single place and the finite bifibre count (Galois orbit argument, then normal closure), and the norm formula that makes pushforward preserve principal divisors - 015 — Places and their extensions
ramification index and inertia degree, the fundamental identity [F′:F] = Σ e f, the divisor calculus it enables, Galois transitivity and constancy, and multiplicativity in towers - 010 — Finite fields, Frobenius, and point counts
rational points as fixed points of the q-power map, the characteristic polynomial T² − a_q T + q and Hasse's bound, the counts over every extension, the rank-2g Tate module with its p-torsion caveat, and the bridgeResidualGaloisRep.IsAttachedTo - 009 — Differentials, residues, and Riemann–Roch
differentials, their orders and divisors, the canonical class and genus, local residues and the residue theorem (so a nonzero function has as many zeros as poles), the Riemann inequality and Riemann–Roch, and the genera-0-to-4 computation inpymath - 008 — Divisors, linear equivalence, and Pic⁰
points as discrete valuation rings, divisors, degree, principal divisors and the residue theorem, Pic/Pic⁰ and the Jacobian of X₀(N) with its Hecke and Galois actions, plus ramification, pullback/pushforward, and the correspondence that becomes T_ℓ
▶ Modular curves, level structure, and uniformization 013 · 018
- 018 — Congruence subgroups, level structures, and invariance
which group acts on which moduli problem (E, ⟨C⟩, P, (P,Q)) and why “invariance” is a congruence; multiplication over ℤ versus reduction mod N, the diamond lift, and the τ ↔ torsion bridge to ±Γ(N) - 013 — Riemann existence for modular curves, and the level-one q-expansion principle
the Riemann existence theorem in function-field form, the compact X₀(N) and the degree-ψ(N) cover, and the separation of the level-one input the proof keeps (Liouville on X(1)) from the level-N connectedness it reconstructs
▶ Automorphic, adelic, and Hecke layers 011 · 012 · 014
- 014 — Hecke operators: cosets, q-expansions, and the two matrices
a Hecke operator as an average of slash actions over the ℓ+1 double-coset representatives; the two matrices the port defines and why they are the whole operator; the q-coefficient rules; and the Hecke-coset polynomial of the PhiGen segment - 012 — Adeles, automorphic representations, and the adelic dictionary
adeles and ideles as restricted products, GL₂(𝔸_F) and K₀(N), automorphic representations and their local factors, the classical↔adelic dictionary, Hecke characters, newvectors and conductor — with the unformalised restricted tensor product flagged - 011 — Deformations, Hecke algebras, and R = T
deformations and the universal deformation ring, the Hecke algebra as a ring, the map R → T built from Eichler–Shimura, and what R = T asserts (the numerical criterion plus Taylor–Wiles patching)
▶ The primer and level one 001–007
- 007 — The Weil pairing
the six laws and FLT'sIsWeilPairing, det ρ = cyclotomic ⇒ oddness, the divisorial definition and Miller's algorithm, the characteristic-zero formula on ℂ/Λ, Frobenius, and the FLT uses - 006 — The modular equation: integrality and splitting
Φ_N and its zero locus, integral coefficients by Galois descent, the prime-level splitting and coset slots, and a p = 3 example - 005 — Cyclic isogenies, congruence level, and the j-invariant
tori as lattices, the moduli reading of j, cyclic isogenies and the p+1 quotient curves, the Dedekind count ψ(N), and Γ₀(N) - 004 — The j-invariant: its q-expansion and first properties
where E₄ and Δ/q come from, the computation of q⁻¹ + 744 + 196884q + ⋯, integrality, and the first properties - 003 — No level-2 weight-2 cusp forms
the index [SL₂(ℤ) : Γ₀(2)] = 3, the norm, and the level-one vanishing down to maximum modulus - 002 — Modular forms at the mathlib level
theSlashInvariantForm/ModularForm/CuspFormchain, q-expansions, the inventory of what mathlib lacks, and the Hecke algebra FLT builds instead - 001 — Field extensions and Galois basics
the field and Galois theory every later note assumes, and the Lean encoding ofAlgebratowers,K ≃ₐ[S] K, and the Galois action on modules
Reading the FLT proof
- anthropics/fermats-last-theorem — the formalisation.
Citations throughout these notes are pinned to the commit
aa2d8b3, because/mainmoves. - Annotated docs — the author's rendered static site
(GitHub's 1000-file directory cap breaks browsing
html/def/). - PROOF-PATH.md — the route through the pin; where this prose and the Lean differ, the Lean is right.