AI 中文总结
本文解决《库罗夫卡笔记本》中八个群论问题，包括构建特定群、证明元素乘积取值情况、说明群阶与统计量不能确定单性、构造算子，还涉及确定生成群、证明幂图性质、探讨子群格情况及反驳秩不等式，且由形式推理主体在Lean中完成。
AI 中文摘要
《库罗夫卡笔记本》是群论中一系列长期存在的开放问题集。本文给出了其中八个问题的解决方案。构建了一个恰好有两个极大局部可解正规子群的群，证明对于每个\(1 \le k\le n!\)，存在一个包含\(n\)个不同元素的群，其\(n!\)个有序乘积恰好取\(k\)个不同值。还给出例子表明群阶与统计量\(\sum_g\varphi(\lvert g\rvert)\)不能确定单性，并在非阿贝尔群上构造了一个满射非单射的罗塔 - 巴克斯特算子。此外，确定了由模至多为\(k\)的类换位生成的群，证明有限群的幂图若是余图则是弦图，表明右可序群的右相对凸子群不一定构成其子群格的子格，反驳了关于某些\(p\)-群扩张的一个拟议的秩不等式。所有这些解决方案均由Harmonic开发的形式推理主体Aristotle在Lean中自主发现并形式验证。
英文摘要
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φ(\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.
Comments21 pages. Lean 4 formalisation: https://github.com/pitmonticone/Kourovka. v2: Expands the appendix with an account on problem selection and adds the MathOverflow provenance of Problem 18.50
