Farrel Jones Conjecture

### What is the conjecture

For a group $G$, the assembly maps
$$H_n^G(EG; K) \to K_n(\mathbb{Z}[G])$$
and
$$H_n^G(EG; L) \to L_n(\mathbb{Z}[G])$$
are isomorphisms in the $K$-theory and $L$-theory of group rings.

**Sources:**
- https://en.wikipedia.org/wiki/Farrell%E2%80%93Jones_conjecture, https://arxiv.org/abs/math/0703548, https://www.mpim-bonn.mpg.de/node/10826, https://link.springer.com/chapter/10.1007/978-3-319-43674-6_1

### Prerequisites needed

**Formalizability Rating:** 4/5 (as of 2026-01-20)

The Farrell-Jones conjecture requires substantial infrastructure beyond current Mathlib. While basic definitions for K-theory and group theory exist, the conjecture involves: (1) equivariant K-theory and L-theory with respect to families of subgroups, (2) equivariant homology groups and classifying spaces for families, (3) assembly maps that require cohomological machinery. These are advanced topics in algebraic topology and algebraic K-theory that would require significant new theory development beyond what is currently in Mathlib.

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

* ams-19
* ams-20
* ams-55

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

Created by AI, edited and reviewed by me.

Start by reviewing the repository’s existing Lean conjecture statements and the cited sources for the Farrell–Jones conjecture. Determine whether the required equivariant K-theory, L-theory, homology, classifying-space, and assembly-map infrastructure exists; done would mean adding a formal statement once those prerequisites are available.

Written by the indexing model from the issue text.