AI and the Langlands Program: From Verification to Discovery

The Langlands Program is a centerpiece of modern mathematics—celebrated for its beauty, its difficulty, and its far-reaching applications. It was a key ingredient in the proof of Fermat's Last Theorem. It connects number theory, algebraic geometry, representation theory, and harmonic analysis in ways that continue to reshape each of these fields.

In 2024, Dennis Gaitsgory and collaborators completed a proof of the (categorical, unramified) Geometric Langlands Conjecture. The proof spans over 1,000 pages across five papers. It has been accepted by the mathematical community—Gaitsgory was awarded the Breakthrough Prize for this work—but it is far from digested. Very few mathematicians have read the full argument end to end. The techniques it introduces are powerful but dense, and the connections to other parts of the Langlands Program remain only partially understood.

We think this makes it a perfect test for machine intelligence.

Most approaches to evaluating AI mathematical reasoning fall into two categories: solving known problems (competition mathematics, textbook exercises) or attempting open problems with unknown approaches (such as Erdős conjectures or Millennium Prize problems). Both have limitations. Known problems test pattern matching as much as reasoning. Open problems with no known strategy offer no gradient—either the model finds a proof or it doesn't.

We propose a third paradigm: theory-building conjectures where the proof architecture is known in a closely related setting and the challenge is to verify, simplify, and transfer it. Concretely:

• Simplify and streamline existing methods — Can an AI system help verify and formalize Gaitsgory's proof, identifying redundancies, clarifying dependencies, and producing machine-checkable components?
• Transfer methods to new contexts — Can an AI system help port the proof architecture to the ℓ-adic and p-adic settings, producing genuinely new and exciting mathematics?

This is closer to how mathematics actually progresses. The most impactful developments are rarely isolated solutions to isolated problems—they are new frameworks that unlock entire research programs. An AI system that can assist with this kind of work is qualitatively different from one that solves competition problems.

The repository, available at github.com/przchojecki/langlands, is organized around three goals:

Goal 1: Atlas of the Gaitsgory proof

We are building a structured atlas of claims in Gaitsgory's five-paper proof series (GLC I–V). This means extracting every definition, lemma, and theorem into a machine-readable format, normalizing notation across papers, and constructing a dependency DAG—a graph that makes the logical structure of the proof explicit and navigable.

The aim is not to formalize from scratch in Lean (current proof assistant ecosystems lack the infrastructure for derived algebraic geometry at this scale), but to build toward formalization incrementally: starting with interface-level lemmas (adjunctions, monads, compactness patterns), then moving deeper as libraries mature. LLMs serve as parsers, librarians, and red-team tools—spotting missing hypotheses, checking functor directions, and flagging hidden dependencies.

Goal 2: Blueprint for ℓ-adic local Langlands (ℓ ≠ p)

The repository includes a TeX blueprint (ladicgeom.tex) that ports the Gaitsgory proof architecture into the Fargues–Scholze setting on the Fargues–Fontaine curve. This is where the real excitement begins: the categorical geometrization conjecture of Fargues–Scholze proposes an equivalence between ℓ-adic sheaves on the v-stack Bun_G and coherent sheaves with nilpotent singular support on a spectral parameter stack—mirroring the structure of Geometric Langlands but in a profoundly different geometric context.

The blueprint maps each step of the Gaitsgory strategy (spectral action, Whittaker generator, parabolic induction, monadicity, gluing) to its proposed ℓ-adic analog, identifying which inputs are known, which require adaptation, and which remain open.

Goal 3: Blueprint for p-adic local Langlands (ℓ = p)

A second blueprint (padicgeom.tex) sketches a conjectural package for the p-adic case, where the coefficient field matches the residue characteristic. This is the hardest and least understood setting—the one where the Emerton–Gee stack replaces classical parameter spaces, and where the relationship between automorphic and spectral sides remains deeply mysterious. The blueprint proposes axioms, works out the GL₂(ℚ_p) test case, and identifies the structural parallels to the geometric and ℓ-adic cases.

LLMs are not trusted oracles in this project. We use them as structured tools with explicit guardrails:

• Parser — Converting TeX and PDF sources into structured claims with metadata
• Librarian — Indexing and cross-referencing results across papers, resolving "same object, different notation" conflicts
• Refactoring assistant — Unifying notation and detecting when different papers state equivalent results
• Formalization copilot — Generating Lean/Coq stubs and interface-level lemma statements
• Red-team tool — Spotting missing hypotheses, hidden finiteness assumptions, and incorrect functor directions

Every generated claim must include a source pointer (paper, section, theorem number), the exact or near-verbatim original statement, an explicit dependency list, and a confidence tag distinguishing verified content from inferred content. If an LLM cannot point to where something appears in the literature, we treat it as a hypothesis, not a fact.

Going forward, we plan to test every new reasoning model on this program to see how far it can get. The Langlands repository offers a gradient of difficulty that most benchmarks lack:

• Level 1: Can the model correctly parse and summarize claims from the Gaitsgory papers?
• Level 2: Can it identify dependencies between results and detect notation conflicts across papers?
• Level 3: Can it generate correct Lean stubs for interface lemmas?
• Level 4: Can it propose plausible analogs of geometric results in the ℓ-adic setting?
• Level 5: Can it identify genuinely new mathematical connections or fill gaps in the blueprints?

This is fundamentally different from asking a model to solve an IMO problem or prove an Erdős conjecture. It tests sustained reasoning over large, interconnected bodies of mathematics—the kind of work that drives actual mathematical progress.

The Langlands Program has shaped mathematics for over fifty years. Its core conjectures connect domains that seem to have no business talking to each other. The recent proof of Geometric Langlands opens the door to transferring those ideas to arithmetic settings where they would have transformative consequences—completing the geometrization of the ℓ-adic local Langlands correspondence as envisioned by Fargues and Scholze, and eventually illuminating the p-adic case.

If AI systems can help with this—not by replacing mathematicians, but by handling the bookkeeping, catching errors, and suggesting structural analogies across 1,000-page proofs—that would represent a genuinely new kind of human-machine collaboration in mathematics. Not artificial intelligence proving theorems, but machine intelligence making mathematicians more effective at the hardest problems in their field.

The repository is open. Contributions—mathematical, engineering, and formalization—are welcome.

Repository: github.com/przchojecki/langlands