On Some Problems from the Kourovka Notebook

Wouter van Doorn, Elias Judin, Pietro Monticone, and Daniel Morrison.

Preprint, July 2026; revised 26 July 2026 (arXiv v2).

We present solutions to eight problems from the Kourovka Notebook, covering subgroup structure, ordered products, Rota–Baxter operators, and power graphs, with accompanying Lean formalizations.

The accompanying repository contains the formal developments and preserves the original Aristotle submissions.

Read the paper on arXiv · PDF · Lean source

Formal proof · CV · Contact