# The Deligne–Drinfeld conjecture

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The Deligne-Drinfeld conjecture](../../preprints/The-Deligne-Drinfeld-conjecture-September-23-2026/paper.pdf)

## Scope

The Deligne–Drinfeld conjecture predicts that the rational Grothendieck–Teichmüller Lie algebra is freely generated by one element in each odd weight $3,5,7,\ldots$. The formalization establishes this for the rational solution space of antisymmetry, the three-term equation, and the four-strand pentagon with the Ihara bracket. It also gives the corresponding continuous isomorphism after completion by weight.

The regularized-transport proposition and graph-complex consequences are not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Deligne–Drinfeld main statement | [DeligneDrinfeld.lean](../ComparatorChallenges/DeligneDrinfeld.lean) |