Sofic Group Conjecture: Is every discrete, countable group sofic?

### What is the conjecture

A discrete group $G$ is **sofic** if there exists a sequence of finite-dimensional unitary representations $\rho_n : G \to U(d_n)$ (where $U(d_n)$ is the group of unitary matrices of size $d_n$) such that for every finite subset $S \subseteq G$ and $\epsilon > 0$, there exists some $n$ such that $\rho_n$ is $\epsilon$-close to being a homomorphism on $S$ in the sense of the uniform metric on homomorphisms.

**The Sofic Group Conjecture** asks: Is every discrete, countable group sofic?

Equivalently, this asks whether every countable discrete group can be approximated arbitrarily well on finite sets by finite-dimensional unitary representations. This is one of the major open problems in the theory of sofic groups and their connection to group rings and the Kadison-Singer conjecture.

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

**Sources:**
- - [Sofic groups (Wikipedia)](https://en.wikipedia.org/wiki/Sofic_group)
- G. Elek and E. Szabó, *Sofic groups* (2005), arXiv preprint math/0511455
- [MathOverflow: Sofic groups](https://mathoverflow.net/questions/tagged/sofic-groups)

### Prerequisites needed

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

Building blocks (1-3; from search results):
- `Matrix.unitaryGroup` and unitary representations in Mathlib
- `Fintype` and finite-dimensional structures for encoding finite groups
- Topological groups and their basic properties

Missing pieces (exactly 2; unclear/absent from search results):
- A comprehensive formalization of sofic groups as a definition (epsilon-approximation by finite-dimensional unitary representations)
- Infrastructure for quantifying over families of finite-dimensional representations and their convergence properties

Rating justification: Sofic groups are a relatively specialized concept not currently in Mathlib. While basic unitary group definitions exist, formalizing the sofic property requires building a new definition around epsilon-approximation of homomorphisms on finite sets by unitary representations. This requires moderate infrastructure development beyond simple combination of existing Mathlib concepts.

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

* ams-20
* ams-37

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