On Some Problems from the Kourovka Notebook
Wouter van Doorn, Elias Judin, Pietro Monticone, Daniel Morrison
math.GR
Jul 20, 2026 · v1
math.CO
TL;DR
Eight open Kourovka Notebook group-theory problems were autonomously solved 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 is a long-standing collection of open problems in group theory, several of which remained unsolved. The challenge is to both discover and rigorously verify solutions to such problems.
Approach
Eight problems from the Kourovka Notebook were addressed, spanning maximal locally soluble normal subgroups, permuted product cardinalities, totient sums and simplicity, Rota-Baxter operators, class transposition groups, power graphs, and right-relatively convex subgroups. Each solution—as proof, counterexample, or construction—was autonomously discovered by Aristotle, a formal reasoning agent developed by Harmonic. All solutions were formalized and machine-checked in Lean 4.
Results
Solutions to all eight problems are presented, including constructing a group with exactly two maximal locally soluble normal subgroups, groups realizing any prescribed number of permuted products, and a surjective non-injective Rota-Baxter operator on a non-abelian group; the group generated by horizontal class transpositions of moduli at most k is shown isomorphic to the symmetric group on lcm(2,...,k).
