Baum–Connes conjecture

### What is the conjecture

Let $G$ be a discrete group. The **assembly map** is a homomorphism $$\mu: K_*^{\text{top}}(G) \to K_*(C_r^*(G))$$ from the topological K-theory of $G$ to the K-theory of the reduced group C*-algebra $C_r^*(G)$, defined via the Kasparov descent construction.

The **Baum–Connes conjecture** asserts that this assembly map is an isomorphism for every discrete group $G$. Equivalently, the assembly map is both injective and surjective.

The conjecture is known to hold for several classes of groups, including:
- Compact groups
- Abelian groups
- Lie groups with finitely many connected components
- Groups with the Haagerup property (a-T-menable groups)
- Discrete cocompact subgroups of real Lie groups of real rank 1

However, a counterexample to the **Baum–Connes conjecture with coefficients** was discovered in 2002 by Higson, Lafforgue, and Skandalis. The conjecture for the coefficient-free case remains open.

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

**Sources:**
- https://en.wikipedia.org/wiki/Baum%E2%80%93Connes_conjecture, https://ncatlab.org/nlab/show/Baum-Connes+conjecture, https://arxiv.org/abs/1905.10081, https://chatterj.perso.math.cnrs.fr/papers/Valette.pdf

### Prerequisites needed

**Formalizability Rating:** 5/5 (0 is best) (as of 2026-02-04)

Building blocks (1-3; from search results):
- `K-theory` and `KK-theory` (Mathlib has basic K-theory infrastructure)
- Topological groups and group C*-algebras (Mathlib has group C*-algebra definitions in `Analysis.CstarAlgebra.Nnnorm`)
- Assembly maps and index theory constructions (partially available)

Missing pieces (exactly 2; unclear/absent from search results):
- Equivariant K-theory and equivariant KK-theory framework (Kasparov descent constructions)
- Rigorous formalization of the reduced group C*-algebra as a functor from groups to C*-algebras with its functorial properties

Rating justification (1-2 sentences): The basic objects (groups, C*-algebras, K-theory) exist or have partial infrastructure in Mathlib, but formalizing the assembly map requires substantial development of equivariant KK-theory and the descent machinery, which is not standard in Mathlib. This is a moderate-to-significant infrastructure lift.

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

* ams-19
* ams-46
* ams-47

### 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.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

No target files, tests, or entry points are identified. Start by reviewing existing K-theory, C*-algebra, and related formalizations in the repository and Mathlib, then assess the missing equivariant K-theory and reduced group C*-algebra infrastructure. Done means the Baum–Connes conjecture is stated rigorously in Lean.

Written by the indexing model from the issue text.