On Some Problems from the Kourovka Notebook
Wouter van Doorn, Elias Judin, Pietro Monticone, Daniel Morrison
math.GR
Jul 20, 2026 · v2
math.CO
TL;DR
Solutions to eight Kourovka Notebook group theory problems were autonomously discovered and formally verified in Lean 4 by Harmonic's Aristotle agent.
Abstract
The Kourovka Notebook is a long-running collection of open problems in group theory. In this paper we present solutions to eight of its problems. We construct a group with exactly two maximal locally soluble normal subgroups and show that, for every $1 \le k\le n!$, there is a group containing $n$ distinct elements whose $n!$ ordered products take exactly $k$ distinct values. We also give examples showing that group order together with the statistic $\sum_g\varphi(\lvert g\rvert)$ does not determine simplicity, and we construct a surjective non-injective Rota-Baxter operator on a non-abelian group. Further, we determine the group generated by the class transpositions of moduli at most $k$, prove that every power graph of a finite group that is a cograph is chordal, show that the right-relatively convex subgroups of a right-orderable group need not form a sublattice of its subgroup lattice, and disprove a proposed rank inequality for certain $p$-group extensions. All of these solutions were autonomously discovered and formally verified in Lean by Aristotle, a formal reasoning agent developed by Harmonic.
Problem
The Kourovka Notebook collects open problems in group theory. Eight of them remained unresolved, including one posed in 1969 on whether the number of maximal locally soluble normal subgroups is always one or infinite.
Approach
Aristotle, a formal reasoning agent developed by Harmonic, autonomously developed the solutions and formalized them in Lean 4. The solutions take the form of proofs, counterexamples, and constructions. The paper presents them in conventional mathematical prose and describes the role of formalization and autonomous agents in finding them.
Results
The constructions include a group with exactly two maximal locally soluble normal subgroups and groups realizing every k ≤ n! distinct values among ordered products. Further results are a non-simple group of order 6048 sharing the totient sum of PSU(3,3), and a surjective non-injective Rota–Baxter operator on a non-abelian group. The paper also proves that CT_(k) ≅ S_{lcm(2..k)} for k≥4 and that cograph power graphs are chordal. Finally, it shows that right-relatively convex subgroups need not form a sublattice and disproves a proposed rank inequality for certain p-group extensions.
