Fermat's Last Theorem Blueprint

Blueprint Summary🔗

Overview
Total entries238completed: 141; deps incomplete: 27; sorries: 10; no proof: 43
Ready now44Entries with an actionable next formalization step.
Fully closed141Local code and prerequisite closure are both complete.
Actionable priorities30Entries ready now and already unlocking downstream work.
Current blockers10Missing external or incomplete Lean declarations.
Missing informal coverage2Entries with Lean code but missing an informal statement or proof block.
Actionable priorities (30)
Current blockers (10)
Missing informal coverage (2)
Entry index (238)
Definitions51completed: 33; deps incomplete: 1; sorries: 0; no proof: 0
Lemmas91completed: 73; deps incomplete: 6; sorries: 1; no proof: 11
Theorems74completed: 25; deps incomplete: 15; sorries: 9; no proof: 25
Corollaries22completed: 10; deps incomplete: 5; sorries: 0; no proof: 7
Informal-only entries59
Definition Index (51)
Theorem / Proposition / Lemma / Corollary Index (187)
By parent groups (12)
Finite and infinite adeles, with local compactness and base change. (43)
Frobenius elements, now merged into mathlib. (10)
Hecke operators via the double-coset formalism. (19)
The modularity lifting theorems. (2)
Background results needed elsewhere in the blueprint. (17)
Reducibility of Frey-curve p-torsion. (7)
Haar characters under linear automorphisms. (37)
Fujisaki's lemma and adelic compactness. (11)
Automorphic forms and Langlands for GLn over Q. (2)
Quaternion algebras for modularity lifting. (1)
Initial reductions of Fermat's Last Theorem. (8)
A worked example of a quaternionic automorphic form. (28)
Dependency insights
Statement-used entries119Entries reused in statement dependencies.
Proof-used entries73Entries reused in proof-only dependencies.
Tracked parent groups12Grouped health rollups for parents with more than one child entry.
Most used in statements (119)
Most used in proofs (73)
Group health (12)
  • Background results needed elsewhere in the blueprint.bestiary_appendix
    Grouped view over entries sharing the same parent.
    total: 29closed: 0local-only: 0ready: 13blocked: 16incomplete Lean: 0unlock score: 127
    Next: manifold_on_algebraic_variety_points stage: statementdownstream unlocks: 11
  • Reducibility of Frey-curve p-torsion.hardly_ramified_program
    Grouped view over entries sharing the same parent.
    total: 8closed: 1local-only: 0ready: 7blocked: 0incomplete Lean: 7unlock score: 18
    Next: hardly_ramified_mod3_reducible stage: proofdownstream unlocks: 3
  • Finite and infinite adeles, with local compactness and base change.adele_project
    Grouped view over entries sharing the same parent.
    total: 49closed: 31local-only: 6ready: 6blocked: 6incomplete Lean: 0unlock score: 268
    Next: pi_tensorProduct_of_finitePresentation stage: proofdownstream unlocks: 10
  • Frobenius elements, now merged into mathlib.frobenius_project
    Grouped view over entries sharing the same parent.
    total: 12closed: 7local-only: 1ready: 4blocked: 0incomplete Lean: 0unlock score: 35
    Next: fixed_of_fixed1_aux1 stage: proofdownstream unlocks: 4
  • Hecke operators via the double-coset formalism.hecke_operator_project
    Grouped view over entries sharing the same parent.
    total: 20closed: 15local-only: 1ready: 4blocked: 0incomplete Lean: 0unlock score: 19
    Next: «nolean-compactopen-U1p» stage: proofdownstream unlocks: 0
  • A worked example of a quaternionic automorphic form.automorphic_example_program
    Grouped view over entries sharing the same parent.
    total: 35closed: 31local-only: 1ready: 3blocked: 0incomplete Lean: 2unlock score: 88
    Next: «HurwitzRatHat.canonicalForm» stage: proofdownstream unlocks: 1
  • Automorphic forms and Langlands for GLn over Q.gln_langlands_program
    Grouped view over entries sharing the same parent.
    total: 10closed: 3local-only: 1ready: 3blocked: 3incomplete Lean: 0unlock score: 13
    Next: instLieAlgebraAction stage: statementdownstream unlocks: 4
  • The modularity lifting theorems.modularity_lifting_program
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 0ready: 2blocked: 0incomplete Lean: 0unlock score: 0
    Next: «IsCentralSimple.baseChange» stage: proofdownstream unlocks: 0
  • Initial reductions of Fermat's Last Theorem.first_reductions
    Grouped view over entries sharing the same parent.
    total: 10closed: 7local-only: 2ready: 1blocked: 0incomplete Lean: 1unlock score: 21
    Next: Wiles_Frey stage: proofdownstream unlocks: 2
  • Haar characters under linear automorphisms.haar_character_project
    Grouped view over entries sharing the same parent.
    total: 39closed: 30local-only: 9ready: 0blocked: 0incomplete Lean: 0unlock score: 398
    Next: no ready child currently unlocks downstream work.
  • Show all 2 more groups
    • Fujisaki's lemma and adelic compactness.fujisaki_project
      Grouped view over entries sharing the same parent.
      total: 16closed: 11local-only: 5ready: 0blocked: 0incomplete Lean: 0unlock score: 109
      Next: no ready child currently unlocks downstream work.
    • Quaternion algebras for modularity lifting.quaternion_algebra_project
      Grouped view over entries sharing the same parent.
      total: 6closed: 5local-only: 1ready: 0blocked: 0incomplete Lean: 0unlock score: 15
      Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner238
Missing effort238
Untagged238
Missing owner (238)
Missing effort (238)
Untagged (238)
Structure and coverage
Informal-only59Statements with no associated Lean code yet.
Ready to formalize44Entries with an actionable next formalization step.
Formalized, ancestors open27Local Lean work is done, but prerequisite closure is still open.
Fully closed141Local code and ancestor closure are both complete.
Blocked or incomplete26Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (170)
No prerequisites (68)
No dependents (58)
Proof debt hotspots (3)
  • Reducibility of Frey-curve p-torsion.hardly_ramified_program
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 7incomplete decls: 7missing decls: 0total debt: 7
  • A worked example of a quaternionic automorphic form.automorphic_example_program
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 2incomplete decls: 2missing decls: 0total debt: 2
  • Initial reductions of Fermat's Last Theorem.first_reductions
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1