The $D_5$ problem
ENRU

Timeline

What was done and when, latest first.

  1. 18 October 2026
    • 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).
  2. 17 October 2026
    • The group analogue of Theorem C: $D_7=1$ for the plateau group; the first search at $c=4$; at $c=5$, $D_7\ne1$ but $D_8\cap\gamma_5=1$.
    • Order $3^8$: the full scan, $904$ non-metabelian groups, $D_5=1$ in all.
    • Order $3^9$: the $p$-cover filter, $62\,245$ candidates, $D_5=1$ in all; rank $5$ excluded on paper.
    • On paper: $D_5=\gamma_5$ for $Q/\gamma_2$ of exponent $3$; the Lie-ring lemma; $P^{*\prime\prime}=1$. Two independent line-by-line reviews.
  3. 16 October 2026
    • Order $2^{10}$ closed: the minimal-counterexample lemma, ANUPQ, $3400$ candidates.
    • Lossless pruning of the $2$-group tree for $2^{11}$; ranks $2$–$3$ and $\ge8$ closed.
    • $2^{11}$, rank $4$: $52\,568$ candidates, all with $D_4=D_5=1$.
  4. 15 October 2026
    • Exact computation of $D_n$ for small $p$-groups: all $2$-groups up to $2^7$, $2^8$ of class $\ge3$, metabelian $2^9$ of class $3$, $3$-groups up to $3^6$.
    • Tahara's bound checked against the original; no $3$-torsion up to $3^7$ (Gupta–Tahara).
    • Truncated Magnus algebra: quotients of Rips-type groups, $D_4\ne1$ at $2^{84}$, $2^{90}$, $2^{107}$ proved, $D_5=1$.
  5. 14 October 2026
    • The Lean formalization of Ionin–Mikhailov–Petrov audited (build, axioms).
    • Group dimension subgroups in Lean: $\gamma_n\subseteq D_n$, $D_2=\gamma_2$, the $D_5$ question stated.
    • Paper draft: the reduction to $2$-groups of class $3$; where the Lie-ring proof does not transfer.