Formalize Arthur's conjectures on automorphic representations

### What is the conjecture

Arthur's conjectures, formulated by James Arthur in the 1980s, provide a framework for parametrizing automorphic representations of reductive groups. Let $G$ be a reductive group over a number field, and let $\widehat{G}$ denote the Langlands dual group. An L-parameter is an equivalence class of admissible homomorphisms $\varphi : L_F \to \widehat{G}(\mathbb{C})$, where $L_F$ is the Langlands group (a modification of the Galois group).

Arthur's conjectures assert that automorphic representations of $G(\mathbb{A}_F)$ (where $\mathbb{A}_F$ is the adele ring) can be classified and grouped into finite sets called L-packets, each corresponding to a single L-parameter $\varphi$. The conjectures specifically predict:

1. Every automorphic representation belongs to exactly one L-packet
2. Each L-packet corresponds to a unique L-parameter
3. The structure of L-packets is governed by the representation theory of the component group of the centralizer of $\varphi$ in $\widehat{G}$

For classical groups (orthogonal, symplectic, and unitary groups), the conjectures relate automorphic representations to global Galois parameters, establishing a deep connection between number theory and representation theory that unifies and extends earlier results on functoriality and L-functions.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Arthur%27s_conjectures, https://www.math.toronto.edu/arthur/, https://www.claymath.org/library/cw/arthur/pdf/34.pdf, https://arxiv.org/abs/2204.04994

### Prerequisites needed

**Formalizability Rating:** 5/5 (0 is best) (as of 2026-03-14)

Building blocks (1-3; from search results):
- `Group theory and representation theory` are available in Mathlib (basic groups, representations)
- `Number theory foundations` (fields, number fields) exist in Mathlib
- `Category theory and homological algebra` (18 in Mathlib) provide foundational categorical structures

Missing pieces (exactly 2; unclear/absent from search results):
- `Adelic groups and automorphic representations`: Complex infrastructure for adeles, adelization, and the theory of automorphic forms is not present in Mathlib. Defining the space of automorphic representations requires substantial new theory.
- `Langlands duality and L-parameters`: The Langlands group, L-parameters, and the notion of L-packets require development of Galois theory beyond current Mathlib scope, plus representation-theoretic machinery specific to the Langlands program.

Rating justification: Stating Arthur's conjectures requires non-trivial new definitions for adeles, automorphic representations, L-parameters, and L-packets. While basic group representation theory exists, the specialized infrastructure for the Langlands program is largely absent, making this a significant formalization effort.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-11
* ams-20
* ams-22

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)