Isomorphism Problem of Coxeter Groups

### What is the conjecture

A **Coxeter group** is a group generated by reflections, defined by a Coxeter matrix $(m_{ij})_{i,j \in S}$ or Coxeter diagram. The **isomorphism problem for Coxeter groups** asks: Given two Coxeter groups $W$ and $W'$ specified by their Coxeter matrices (or diagrams), determine whether they are isomorphic as abstract groups—that is, whether there exists a group isomorphism $\phi: W \to W'$.

This is a classical open problem in combinatorial group theory. While the problem has been resolved for certain special classes of Coxeter groups (e.g., finitely generated chordal Coxeter groups, triangle groups), the general problem 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/Isomorphism_problem_of_Coxeter_groups
- https://arxiv.org/abs/math/0506572
- https://www.worldscientific.com/worldscibooks/10.1142/p385

### Prerequisites needed

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

Building blocks (from search results):
- Group isomorphism (exists in Mathlib via `Group` and `Equiv`)
- Matrix representations (available in Mathlib)
- General group theory infrastructure

Missing pieces:
- Formal definition of Coxeter groups and their presentations via Coxeter matrices/diagrams in Lean
- Framework for defining groups from Coxeter data

Rating justification: Coxeter group theory is not present in Mathlib, requiring significant foundational work to define Coxeter groups themselves. Once that infrastructure exists, stating the isomorphism problem is straightforward using existing group-theoretic machinery.

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

* ams-20

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