Fermat's Last Theorem Blueprint

Blueprint Summary🔗

Overview
Total entries232completed: 136; deps incomplete: 22; sorries: 9; no proof: 47
Ready now13Entries whose next formalization step is currently unblocked.
Fully closed136Local code and prerequisite closure are both complete.
Actionable priorities33Entries 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 (33)
Current blockers (9)
Missing informal coverage (2)
Entry index (232)
Definitions51completed: 32; deps incomplete: 1; sorries: 0; no proof: 0
Lemmas89completed: 71; deps incomplete: 3; sorries: 1; no proof: 14
Theorems73completed: 25; deps incomplete: 14; sorries: 8; no proof: 26
Corollaries19completed: 8; deps incomplete: 4; sorries: 0; no proof: 7
Informal-only entries61
Definition Index (51)
Theorem / Lemma / Corollary Index (181)
By parent groups (12)
The adele miniproject develops the finite adeles, infinite adeles, and full adeles of a number field together with the local compactness and base-change results needed later in the project. (42)
This miniproject has been a success: the main results are sorry-free and merged into mathlib. As a result there will be no more work on this miniproject in the FLT repo. Below is a fairly detailed sketch of the argument used. (10)
This miniproject packages the abstract double-coset formalism and then applies it to spaces of automorphic forms. (20)
Stating the modularity lifting theorems. (2)
In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (17)
Reducibility of p -torsion of the Frey curve. (7)
This miniproject develops the API around how additive Haar measure changes under linear automorphisms, especially on locally compact topological rings. (28)
Fujisaki's lemma packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms. (11)
This chapter came from discussions between Patrick, Mario and myself, all currently visiting the Hausdorff Research Institute for Mathematics in Bonn. The ultimate goal is to formally state some version of the global Langlands reciprocity conjectures for GL_n over Q . (2)
Miniproject: Quaternion algebras. (1)
First reductions of the problem. (8)
The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story. (28)
Dependency insights
Statement-used entries116Entries reused in statement dependencies.
Proof-used entries68Entries reused in proof-only dependencies.
Tracked parent groups12Grouped health rollups for parents with more than one child entry.
Most used in statements (116)
Most used in proofs (68)
Group health (12)
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.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
  • The adele miniproject develops the finite adeles, infinite adeles, and full adeles of a number field together with the local compactness and base-change results needed later in the project.adele_project
    Grouped view over entries sharing the same parent.
    total: 48closed: 31local-only: 5ready: 6blocked: 6incomplete Lean: 0unlock score: 241
    Next: pi_tensorProduct_of_finitePresentation stage: proofdownstream unlocks: 9
  • Reducibility of p -torsion of the Frey curve.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
  • This miniproject has been a success: the main results are sorry-free and merged into mathlib. As a result there will be no more work on this miniproject in the FLT repo. Below is a fairly detailed sketch of the argument used.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
  • This miniproject packages the abstract double-coset formalism and then applies it to spaces of automorphic forms.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-GL2» stage: statementdownstream unlocks: 1
  • This chapter came from discussions between Patrick, Mario and myself, all currently visiting the Hausdorff Research Institute for Mathematics in Bonn. The ultimate goal is to formally state some version of the global Langlands reciprocity conjectures for GL_n 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
  • The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.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
  • Stating 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.
  • This miniproject develops the API around how additive Haar measure changes under linear automorphisms, especially on locally compact topological rings.haar_character_project
    Grouped view over entries sharing the same parent.
    total: 30closed: 26local-only: 3ready: 1blocked: 0incomplete Lean: 0unlock score: 267
    Next: «NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul» stage: statementdownstream unlocks: 6
  • First reductions of the problem.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 packages the adelic compactness statement that underlies the finiteness of many spaces of quaternionic automorphic forms.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.
    • Miniproject: Quaternion algebras.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 owner232
Missing effort232
Untagged232
Missing owner (232)
Missing effort (232)
Untagged (232)
Structure and coverage
Informal-only61Statements with no associated Lean code yet.
Ready to formalize13Entries whose next step is currently unblocked.
Formalized, ancestors open22Local Lean work is done, but prerequisite closure is still open.
Fully closed136Local code and ancestor closure are both complete.
Heaviest prerequisites (160)
No prerequisites (72)
No dependents (59)
Proof debt hotspots (3)
  • Reducibility of p -torsion of the Frey curve.hardly_ramified_program
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 6incomplete decls: 6missing decls: 0total debt: 6
  • The old chapter develops one explicit quaternionic automorphic example to guide the general definitions used later in the modularity-lifting story.automorphic_example_program
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 2incomplete decls: 2missing decls: 0total debt: 2
  • First reductions of the problem.first_reductions
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1