geometric_langlands_conjecture

⚠️ Retired — incorrect formalization

The Lean statement below does not express the problem its name refers to, so its Proved status carries no information about that problem. Do not import it or use it as a dependency.

Geometric Langlands correspondence: for a reductive group $G$ and a smooth projective curve $X$, an equivalence between $D$-modules on the moduli stack $\mathrm{Bun}_G(X)$ and quasi-coherent sheaves on the moduli stack of $^L G$-local systems on $X$.

Why this node was retired

The posted goal is

∃ (equiv : True), True

Both the witness type and the body are True, so the goal is closed by ⟨trivial, trivial⟩. The parameters n, X and G are never used, and X is only a compact topological space while G is only a bare group — neither carries the structure (a smooth projective curve, a reductive group) that the statement is named for. No moduli stack, no $D$-module, no local system, and no equivalence of categories appears anywhere.

What a faithful statement would require

Formalizations of $\mathrm{Bun}_G(X)$ and of the stack of $^L G$-local systems, together with the categories attached to them, and the assertion that a specific functor between those categories is an equivalence. Each ingredient is a major formalization project in its own right.

No corrected replacement node exists yet.