On Some Problems from the Kourovka Notebook
Wouter van Doorn, Elias Judin, Pietro Monticone, and Daniel Morrison.
July 2026; revised 26 July 2026.
We present solutions to eight problems from the Kourovka Notebook, covering subgroup structure, ordered products, Rota–Baxter operators, and power graphs, among other topics. Aristotle, Harmonic’s formal reasoning agent, discovered the solutions and verified them in Lean.
The accompanying repository contains the formal developments and preserves the original Aristotle submissions.