Paper draft

Version of 18 October 2026. Read it: in English (21 pp.), in Russian (23 pp.); download the PDF: EN, RU. This is a draft: the status of every statement is marked in the text ([Lean], [paper], [computer], [open]).

Any place of the paper can be linked to: viewer.html#nameddest=thm:small opens the theorem labelled thm:small, viewer.html#page=6 a page; the labels are in the contents below (each entry also has an anchor on this page). The same works with the PDF itself: paper/d5.pdf#nameddest=thm:small.

Abstract

For a group $G$ let $D_n(G)=G\cap(1+\D(G)^n)$ be its integral dimension subgroups and $\gamma_n(G)$ its lower central series. Whether $D_5(G)\subseteq\gamma_4(G)$ for every group is open (Kourovka Notebook, Problem 20.84). For Lie rings the analogous inclusion was recently proved by Ionin, Mikhailov and Petrov, and formally verified in Lean. This note collects what is known, records an elementary reduction of the group question to finite metabelian $2$-groups of class three, analyses which steps of the Lie-ring proof have no group-theoretic counterpart, and reports computational evidence. For $3$-torsion in $D_5/\gamma_5$ we prove $D_5(G)=\gamma_5(G)$ whenever $G/\gamma_2(G)$ is finite and has at most one invariant larger than $3$, and, with a computer search, for all $3$-groups of order at most $3^9$. We do not solve the problem.

Contents

  1. 1. The question p. 1
    question 1 · Question 1.1 ([KM26, Problem 20.84], [IMP26, §1.3])
  2. 2. An elementary reduction p. 1
    question 2 · Prop. 2.1 · Rem. 2.2 (“metabelian” is automatic) · Rem. 2.3 (a bounded form)
  3. 3. The Lie-ring proof and where it does not transfer p. 3
  4. 4. Formalization p. 4
  5. 5. Computations p. 5
    Prop. 5.1 · Lemma 5.2 (minimal counterexample) · Prop. 5.3 · Thm. 5.4 · Rem. 5.5 (pruning the generation tree; MATH-40) · Lemma 5.6 · Prop. 5.7 · Prop. 5.8 · Lemma 5.9
  6. 6. $3$-torsion: orders $3^8$ and $3^9$, and groups with $G/\gamma _2$ of exponent $3$ p. 13
    Lemma 6.1 · Lemma 6.2 (minimal counterexample, $p=3$) · Lemma 6.3 · Rem. 6.4 · Prop. 6.5 · Thm. 6.6 · Rem. 6.7 · Thm. 6.8 · Lemma 6.9 (a filter on parents) · Thm. 6.10 · Rem. 6.11 · Thm. 6.12
  7. 7. Open questions p. 19
  8. References p. 20