GLzero.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

5 declarations, 4 contain sorry, 0 declared as axioms

Proof of a case of the global Langlands conjectures.

Class Field Theory was one of the highlights of 19th century mathematics, linking analysis to arithmetic of extensions of number fields with abelian Galois groups. In the 1960s the main results had been re-interpreted as the GL(1) case of the global Langlands conjectures. The general global Langlands conjectures are for GL(n) for any natural number n, and work over any number field or global function field. Much is known in the function field case (Lafforgue got a Fields Medal for his work on the topic), but the general number field case remains largely open even today. For example we have very few results if the base number field is not totally real or CM. For simplicity, let us stick to GL(n)/Q.

In 1993 Wiles announced his proof of the modularity of semistable elliptic curves over the rationals. The result gave us a way of constructing automorphic forms from Galois representations; refinements of the work by Taylor and others over the next decade led to a profound understanding of the "holomorphic" or "odd" part of global Langlands functoriality for GL(2) over the rationals. Wiles' work used class field theory (in the form of global Tate duality) crucially in a central proof that a deformation ring R was isomorphic to a Hecke algebra T.

The fact that Wiles needed the theory for GL(1) to make progress in the GL(2) case, is surely evidence that at the end of the day the proof for GL(n) is going to be by induction on n. We will thus attempt to prove the global Langlands conjectures for GL(0).

Structure of the proof

We will deduce the global Langlands conjectures for GL(0) from a far stronger theorem, called the classification theorem for automorphic representations for GL(0) over Q. This theorem gives a canonical isomorphism between the space of automorphic representations and the complex numbers. Except in Lean we're not allowed to say "canonical" so instead our "theorem" is a definition of a bijection.

TODO

State them first.

Imports (1)

FLT.GlobalLanglandsConjectures.GLnDefs

Imported by 1 file

FLT.lean

def AutomorphicForm.GLn.Weight.IsTrivial A GLₙ-weight ρ is trivial if it is the one-dimensional trivial representation sorry line 52 source
Source documentation
A GLₙ-weight ρ is trivial if it is the one-dimensional trivial representation.

depends on sorry what this means
Statement uses: Nat, AutomorphicForm.GLn.Weight
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def GLn.Weight.IsTrivial {n : ℕ} (ρ : Weight n) : Prop := sorry -- (ρ = trivial 1d rep)
…
```
Mentions: AutomorphicForm.GLn.Weight
def AutomorphicForm.GL0.ofComplex Make an automorphic form for GL₀/ℚ from a complex number sorry line 62 source
Source documentation
Make an automorphic form for GL₀/ℚ from a complex number

depends on sorry what this means
Statement uses: AutomorphicForm.GLn.Weight, OfNat.ofNat, Nat, Complex, AutomorphicForm.GLn.AutomorphicFormForGLnOverQ
Proof uses: AutomorphicForm.GLn.AutomorphicFormForGLnOverQ.mk, Prod, Matrix.GeneralLinearGroup, Fin, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real
19 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
def ofComplex (c : ℂ) : AutomorphicFormForGLnOverQ 0 ρ := {
…
```
def AutomorphicForm.GL0.classification The classification of automorphic forms for GL₀/ℚ: they are in bijection with ℂ line 94 source
Source documentation
The classification of automorphic forms for GL₀/ℚ: they are in bijection with ℂ.

depends on sorry what this means
Statement uses: AutomorphicForm.GLn.Weight, OfNat.ofNat, Nat, Equiv, AutomorphicForm.GLn.AutomorphicFormForGLnOverQ, Complex
Proof uses: Equiv.mk, AutomorphicForm.GLn.AutomorphicFormForGLnOverQ.toFun, Prod, Matrix.GeneralLinearGroup, Fin, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Matrix, AutomorphicForm.GL0.ofComplex
22 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
noncomputable def classification : AutomorphicFormForGLnOverQ 0 ρ ≃ ℂ := {
…
```
def AutomorphicForm.GLn.ofComplex Make an automorphic form for GLₙ/ℚ of trivial weight ρ from a complex number z, returning the constant function with value z sorry line 120 source
Source documentation
Make an automorphic form for GLₙ/ℚ of trivial weight ρ from a complex number z, returning the constant function with value z.

depends on sorry what this means
Statement uses: Complex, Nat, AutomorphicForm.GLn.Weight, AutomorphicForm.GLn.Weight.IsTrivial, AutomorphicForm.GLn.AutomorphicFormForGLnOverQ
Proof uses: AutomorphicForm.GLn.AutomorphicFormForGLnOverQ.mk, Prod, Matrix.GeneralLinearGroup, Fin, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, sorryAx, Lean.Name, AutomorphicForm.GLn.IsSmooth, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Eq, AutomorphicForm.GLn.IsSlowlyIncreasing, Exists, Subgroup and 2 more
18 instances, coercions and auxiliary constants left out.
```
def ofComplex (z : ℂ) {n : ℕ} (ρ : Weight n) (hρ : ρ.IsTrivial) :
    AutomorphicFormForGLnOverQ n ρ where
…
```
Mentions: AutomorphicForm.GLn.Weight, AutomorphicForm.GLn.AutomorphicFormForGLnOverQ
def AutomorphicForm.GLn.classification The classification of automorphic forms for GL₀/ℚ of weight ρ: they are in bijection with ℂ sorry line 132 source
Source documentation
The classification of automorphic forms for GL₀/ℚ of weight ρ: they are in bijection with ℂ.

depends on sorry what this means
Statement uses: AutomorphicForm.GLn.Weight, OfNat.ofNat, Nat, Equiv, AutomorphicForm.GLn.AutomorphicFormForGLnOverQ, Complex
Proof uses: Equiv.mk, AutomorphicForm.GLn.AutomorphicFormForGLnOverQ.toFun, Prod, Matrix.GeneralLinearGroup, Fin, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Matrix, AutomorphicForm.GLn.ofComplex, sorryAx, Lean.Name, AutomorphicForm.GLn.Weight.IsTrivial, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Function.LeftInverse, Function.RightInverse
20 instances, coercions and auxiliary constants left out.
```
noncomputable def classification (ρ : Weight 0) : AutomorphicFormForGLnOverQ 0 ρ ≃ ℂ where
…
```
Mentions: AutomorphicForm.GLn.Weight, AutomorphicForm.GLn.AutomorphicFormForGLnOverQ