Fermat's Last Theorem Blueprint

Blueprint Summary🔗

Overview
Total entries237completed: 137; deps incomplete: 28; sorries: 9; no proof: 45
Ready now11Entries whose next formalization step is currently unblocked.
Fully closed137Local code and prerequisite closure are both complete.
Actionable priorities32Entries ready now and already unlocking downstream work.
Current blockers9Missing external or incomplete Lean declarations.
Missing informal coverage2Entries with Lean code but missing an informal statement or proof block.
Ready next (32)
Current blockers (9)
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: 15; sorries: 8; no proof: 26
Corollaries22completed: 9; deps incomplete: 6; sorries: 0; no proof: 7
Informal-only entries61
Definition Index (51)
Theorem / 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 entries117Entries 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 (117)
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
  • 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
  • Reducibility of Frey-curve p-torsion.hardly_ramified_program
    Grouped view over entries sharing the same parent.
    total: 8closed: 1local-only: 1ready: 6blocked: 0incomplete Lean: 6unlock score: 39
    Next: hardly_ramified_mod3_reducible stage: proofdownstream unlocks: 6
  • 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: no ready child currently unlocks downstream work.
  • 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
  • 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: no ready child currently unlocks downstream work.
  • 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
  • Initial reductions of Fermat's Last Theorem.first_reductions
    Grouped view over entries sharing the same parent.
    total: 10closed: 6local-only: 3ready: 1blocked: 0incomplete Lean: 1unlock score: 21
    Next: Mazur_Frey stage: proofdownstream unlocks: 2
  • 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: 13
      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-only61Statements with no associated Lean code yet.
Ready to formalize11Entries whose next step is currently unblocked.
Formalized, ancestors open28Local Lean work is done, but prerequisite closure is still open.
Fully closed137Local code and ancestor closure are both complete.
Heaviest prerequisites (168)
No prerequisites (69)
No dependents (60)
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: 6incomplete decls: 6missing decls: 0total debt: 6
  • 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