Eight problems from the Kourovka Notebook solved and formalized in Lean
A formal reasoning agent developed the proof strategies for eight open problems in group theory without human guidance on which mathematical steps to take, and machine-checked every one in Lean 4.
- Lab
- Harmonic
- Model
- Aristotle
- Field
- Mathematics
- Date
- 2026-07-20
- Human collaborators
- Wouter van Doorn, Elias Judin, Pietro Monticone, Daniel Morrison
- Problem posed
- 1969 · open 57 yrs
What was found
The Kourovka Notebook has collected open problems in group theory since 1965, with a new issue every two to four years. Aristotle solved eight of them: 3.46 (a group with exactly two maximal locally soluble normal subgroups), 18.50, 19.25, 20.125 (a surjective non-injective Rota-Baxter operator on a non-abelian group), 21.8, 21.24, 21.147 and 21.150. The oldest first appeared in the third issue in 1969. Solutions take the form of proofs, counterexamples and constructions, each formalized in Lean 4 and published in a companion repository. The authors then informalized the Lean proofs into conventional prose and submitted both to the Notebook editors and the original problem proposers, who accepted them before publication.
Novelty check
The Kourovka Notebook is itself the authoritative open-problems register for group theory, and each of the eight is recorded there as open with a named proposer, so novelty is established by the source of record rather than by a literature search. The authors submitted solutions to the Notebook editors and the problem proposers for acceptance before publishing, and the initial submissions remain in the Notebook's own preprint repository. Problem 3.46 traces to Plotkin's survey question on products of locally soluble normal subgroups, which Baumslag, Kovács and Neumann had partly addressed in the negative.
Caveats and known objections
Not peer reviewed as a journal article, though the individual solutions were accepted by the Kourovka Notebook editors and the problem proposers, which is the relevant gatekeeping for this venue. The autonomy grade rests on the authors' own disclosure: they state Aristotle developed the proof strategies without human guidance about which steps to take, while they monitored its work, intervened when clarifications were needed, and built a library of relevant concepts with it. That library work and the final canonisation for Mathlib upstreaming were done partly by hand. The Lean certificates are the load-bearing evidence and anyone can rerun them; the claim about how the arguments were found rests on the authors' account.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and Autonomous.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and autonomous for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Eight problems from the Kourovka Notebook solved and formalized in Lean. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-07-20-kourovka-notebookBibTeX
@misc{whataifound-harmonic-2026-notebook,
title = {Eight problems from the Kourovka Notebook solved and formalized in Lean},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Harmonic. Verification: Formally verified. Autonomy: Autonomous.},
url = {https://whataifound.org/finding/2026-07-20-kourovka-notebook}
}