The $D_5$ problem: where we are

The question (Kourovka notebook, Problem 20.84). Let $\Delta$ be the augmentation ideal of $\mathbb Z[G]$, $D_n(G)=G\cap(1+\Delta^n)$ the dimension subgroups and $\gamma_n(G)$ the lower central series. Always $\gamma_n\subseteq D_n$, and $D_n=\gamma_n$ for $n\le3$; for $n=4$ this fails (Rips). Is $D_5(G)\subseteq\gamma_4(G)$ for every group?

For Lie rings the answer is yes (Ionin, Mikhailov, Petrov, 2026, formalized in Lean). For groups it is open, and we have not solved it. This site shows what is proved, what is computed, and what is left.

$2$-torsion: $D_5\subseteq\gamma_4$

up to $2^{10}$

True for every finite group whose Sylow $2$-subgroup has order $\le2^{10}$, in particular for all groups of order $<2048$.

Order $2^{11}$: ranks $2$–$4$ and $\ge8$ closed, $5$–$7$ open.

$3$-torsion: $D_5=\gamma_5$

up to $3^9$

No $3$-torsion in $D_5/\gamma_5$ when the Sylow $3$-subgroup has order $\le3^9$.

On paper for all groups whose $G/\gamma_2$ has at most one invariant larger than $3$ (e.g. exponent $3$, or $C_9\times C_3^{s-1}$), of any order.

Lie rings and Lean

proved

$D_5(L)\subseteq\gamma_4(L)$ for Lie rings; the formalization audited. The group question and the reduction to $2$-groups of class $3$ are stated in Lean.

Counterexamples

No computed group has $D_5\ne\gamma_5$; in all of them $D_n=\gamma_n$ for every $n$. Over a hundred thousand candidates, all computations exact.

Coverage map: $2$-groups of class $3$

A cell stands for all $2$-groups of class $3$ of the given order and rank; it is closed when all of them have $D_5=1$. 33 cells are closed and 3 open. More on the coverage map page.

C computer C+P computer + paper P paper ? open. Empty cells: no such groups.

Latest

On paper: $D_5=\gamma_5$ when $Q/\gamma_2$ has at most one invariant larger than $3$ (including $C_9\times C_3^{s-1}$); an independent review found no errors.
References: what Tahara actually announced (p. 173), and the search for his separate paper.
Computer check for $C_9\times C_3^{s-1}$ and $C_{27},C_{81}\times C_3^{s-1}$: $2\,057$ groups, $4\,537$ elements $z$, none in $D_5$.
ANUPQ audit (ispacex.github.io/gap): the $3^9$ descendant step was repeated with the fixed version, and the result is byte-identical.
On paper: $D_n(H\circ E)=D_n(H)$ for central products with $D_8$, $Q_8$ and $M_{2^{k+2}}$ (adjoining a central square root); all $386$ candidates of orders $2^6$–$2^9$ satisfy the conditions. Two independent reviews.
On paper: gluing along a proper subgroup of $Z(E)$ — a lemma on central roots of any degree (Lemma 5.9). The splittings of the $386$ candidates: $20$ split, each has a splitting covered by Prop. 5.8. An independent review and a recount by another method.
Lean: Lemma 5.9 (a central root of any degree) is proved in Lean, with no sorry and only the standard axioms; formalizing the other paper results has started.
Lean: Prop. 5.8 is proved in Lean in all cases ($D_8$, $Q_8$, $M_{2^{k+2}}$), with the ring statement $\mathbb Z[H]\cap\Delta(Q)^n=\Delta(H)^n$; $Q_8$ and $M_{2^{k+2}}$ reduce to $D_8$ through one overgroup $(Q\times\mathbb Z)/\langle(s,-2)\rangle$.
Lean: the reduction (Prop. 2.1, Remark 2.3) is proved modulo explicit hypotheses — the theorems of Passi and Gruenberg and $D_3=\gamma_3$: from class $\le3$ to finitely generated groups and to finite $2$-groups of class $3$; for finite groups Gruenberg's theorem is not needed.
Lean: Lemma 6.3 and Prop. 6.5 ($[\gamma_2,\gamma_2]\subseteq\gamma_5$; a non-metabelian $p$-group of class $4$ and rank $d$ has order $\ge p^{d+5}$) are proved in Lean with no hypotheses; instead of the Lie ring, the group $G/\gamma_5$ and the Hall–Witt identity.
Lean: Theorems 6.6 and 6.8 ($D_5=\gamma_5$ for $G/\gamma_2\cong C_{3^a}\times C_3^{s-1}$) are proved in Lean modulo Tahara's Theorem 6.1, stated as an explicit hypothesis and checked against the scan; both subcases, including the row $s$ of condition (E).

The paper draft (of 18 October 2026): English, Russian (PDF: EN, RU); the whole story is in the timeline.