Fermat's Last Theorem Blueprint

Blueprint Summary🔗

Overview
Total entries237completed: 137; deps incomplete: 25; sorries: 10; no proof: 47
Ready now48Entries with an actionable next formalization step.
Fully closed137Local code and prerequisite closure are both complete.
Actionable priorities32Entries 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 (32)
Current blockers (10)
Missing informal coverage (2)
Entry index (237)
Definitions51completed: 32; deps incomplete: 1; sorries: 0; no proof: 0
Lemmas91completed: 72; deps incomplete: 6; sorries: 1; no proof: 12
Theorems73completed: 24; deps incomplete: 14; sorries: 9; no proof: 26
Corollaries22completed: 9; deps incomplete: 4; sorries: 0; no proof: 9
Informal-only entries63
Definition Index (51)
Theorem / Proposition / Lemma / Corollary Index (186)
By parent groups (12)
Finite and infinite adeles, with local compactness and base change. (42)
Frobenius elements, now merged into mathlib. (10)
Hecke operators via the double-coset formalism. (20)
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. (35)
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 entries118Entries reused in statement dependencies.
Proof-used entries71Entries reused in proof-only dependencies.
Tracked parent groups12Grouped health rollups for parents with more than one child entry.
Most used in statements (118)
Most used in proofs (71)
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: 39
    Next: hardly_ramified_mod3_reducible stage: proofdownstream unlocks: 6
  • Finite and infinite adeles, with local compactness and base change.adele_project
    Grouped view over entries sharing the same parent.
    total: 48closed: 31local-only: 5ready: 6blocked: 6incomplete Lean: 0unlock score: 240
    Next: pi_tensorProduct_of_finitePresentation stage: proofdownstream unlocks: 9
  • 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: 21closed: 16local-only: 1ready: 4blocked: 0incomplete Lean: 0unlock score: 20
    Next: «nolean-compactopen-U1p» stage: proofdownstream unlocks: 0
  • Automorphic forms and Langlands for GLn over Q.gln_langlands_program
    Grouped view over entries sharing the same parent.
    total: 10closed: 2local-only: 1ready: 4blocked: 3incomplete Lean: 0unlock score: 13
    Next: instLieAlgebraAction stage: statementdownstream unlocks: 4
  • 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
  • Initial reductions of Fermat's Last Theorem.first_reductions
    Grouped view over entries sharing the same parent.
    total: 10closed: 6local-only: 1ready: 2blocked: 1incomplete Lean: 1unlock score: 21
    Next: Wiles_Frey stage: proofdownstream unlocks: 2
  • 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
  • Haar characters under linear automorphisms.haar_character_project
    Grouped view over entries sharing the same parent.
    total: 37closed: 27local-only: 9ready: 1blocked: 0incomplete Lean: 0unlock score: 384
    Next: «NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul» stage: statementdownstream unlocks: 6
  • 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 owner237
Missing effort237
Untagged237
Missing owner (237)
Missing effort (237)
Untagged (237)
Structure and coverage
Informal-only63Statements with no associated Lean code yet.
Ready to formalize48Entries with an actionable next formalization step.
Formalized, ancestors open25Local Lean work is done, but prerequisite closure is still open.
Fully closed137Local code and ancestor closure are both complete.
Blocked or incomplete27Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (168)
No prerequisites (69)
No dependents (59)
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