What was already known
An abelian counterexample was already known; the problem authors clarified that the intended question asked for a non-abelian one.
AI involvement
Van Doorn, Judin, Monticone and Morrison report that Aristotle developed the proof strategy and Lean proof without human guidance on mathematical steps. The authors chose problems, supplied infrastructure, refined the formal code, translated the proofs into prose and arranged external review.
The authors say Aristotle developed the new mathematical argument and formal proof strategy without human guidance on the mathematical steps. Humans selected the task, supplied infrastructure, refined the code and wrote the prose account.
Importance
Aristotle’s revised construction supplies a non-abelian counterexample to the intended question.
Limitations
The initial abelian example was already known. The contribution assessed here is the later non-abelian construction after the authors’ clarification.
Technical verification
The companion metadata names declaration kourovka_21_147 and reports a complete Lean proof with zero sorry. This is a source-reported machine check of the scoped theorem; the assessment did not compile the project.
Formal checking
The authors report a Lean 4 proof with zero sorry for declaration kourovka_21_147.
- Checker
- Lean 4
- Scope
- In a non-abelian right-orderable group, the right-relatively convex subgroups need not form a sublattice of its subgroup lattice.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Van Doorn, Judin, Monticone and Morrison translated the formal solution, refined the explanation and present the construction or proof in mathematical prose. This documents human explanation of the central argument.
Correction and publication history
Primary-source review of the scoped Kourovka result, AI contribution, Lean checking, human prose proof and prior baseline. Historical, non-notifying addition.
Read this published revision