Grothendieck-Teichmüller Conjecture

### What is the conjecture

The Grothendieck-Teichmüller conjecture states that the absolute Galois group $\text{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ is isomorphic to the Grothendieck-Teichmüller group $\text{GT}(\mathbb{Q})$.

The Grothendieck-Teichmüller group $\text{GT}(K)$ for a field $K$ of characteristic $0$ is defined as the group of pairs $(\lambda, f)$ where $\lambda \in K^{\times}$ and $f$ is a formal power series in two variables satisfying certain compatibility conditions with the standard free pro-object structure. There exists a natural homomorphism from $\text{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ into $\text{GT}(\mathbb{Q})$, but the conjecture that this map is an isomorphism remains open.

This conjecture is central to arithmetic geometry and represents a key approach to understanding the structure of the absolute Galois group of the rationals.

(This description is intended to be rough and might contain subtle errors / hallucinations; for exact details, refer to the sources.)

(This was mainly a test to include a mathoverflow question.)

**Sources:**
- https://mathoverflow.net/questions/64146/grothendieck-teichm%c3%bcller-conjecture, https://ncatlab.org/nlab/show/Grothendieck-Teichm%C3%BCller+tower, https://people.math.ethz.ch/~wilthoma/docs/grt.pdf, https://aimath.org/WWN/motivesdessins/schneps1.pdf, https://arxiv.org/abs/2503.13006

### Prerequisites needed

**Formalizability Rating:** 5/5 (0 is best) (as of 2026-01-21)

The Grothendieck-Teichmüller group is a highly specialized object in arithmetic geometry that is not currently represented in Mathlib. While Mathlib has basic foundations for Galois groups, profinite groups, and absolute Galois groups, the specific definition of the Grothendieck-Teichmüller group and its required formal structures (free pro-objects, compatibility conditions with dessin d'enfants, etc.) would require substantial new theoretical infrastructure. Formalizing even the statement of the conjecture would require building out significant new theory for GT groups and their relationship to profinite group representations.

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

* ams-11
* ams-12
* 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

No repository file, entry point, or test is named. Start with the linked MathOverflow and reference documents, then inspect the repository's existing conjecture formalizations and prerequisites. Done would require a reviewed Lean statement of the conjecture, but the issue indicates that substantial Grothendieck-Teichmüller infrastructure is still missing.

Written by the indexing model from the issue text.