Kourovka
The 7 problem files in FormalConjectures/Kourovka that state a research or textbook statement, at commit 2055e5ad, one article each.
Their docstrings and Lean statements are quoted from Formal Conjectures (Google DeepMind) at that commit, under its Apache-2.0 license.
TheoremConjecture 1.35(c)#
by A. I. Mal'cev and L. Fuchs
Reference: The Kourovka Notebook
Quoted from FormalConjectures/Kourovka/1_35c.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open.
Kourovka.«1.35c».kourovka_1_35c
Open: stated without proof.
Do there exist simple pro-orderable groups?
theorem kourovka_1_35c :
∃ (G : Type) (_ : Group G), IsSimpleGroup G ∧ ProOrderable G
Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Kourovka/1_35c.lean, line 53.
Sources
TheoremConjecture 1.40#
by Sh. S. Kemkhadze
Is a group a nilgroup if it is the product of two normal nilsubgroups?
Here a nilgroup (Engel group) is a group in which every element is an Engel element. This is the Engel-group analogue of Fitting's theorem, which guarantees that the product of two normal nilpotent subgroups is nilpotent.
Reference: The Kourovka Notebook
Quoted from FormalConjectures/Kourovka/1_40.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open.
Kourovka.«1.40».kourovka_1_40
Open: stated without proof.
Is a group a nilgroup if it is the product of two normal nilsubgroups?
Since \(H\) and \(K\) are normal, the product \(HK\) coincides with the join \(H \sqcup K\), so "\(G\) is the product of \(H\) and \(K\)" is stated as \(H \sqcup K = G\).
theorem kourovka_1_40 :
∀ (G : Type) [Group G] (H K : Subgroup G),
H.Normal → K.Normal → IsEngelGroup H → IsEngelGroup K → H ⊔ K = ⊤ →
IsEngelGroup G
Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Kourovka/1_40.lean, line 66.
Sources
TheoremConjecture 1.74 (Minimal topological groups)#
by V. P. Platonov
Describe all "minimal topological groups", that is, non-discrete Hausdorff topological groups all of whose proper closed subgroups are discrete. The minimal locally compact groups can be described without much effort, but the problem is probably complicated in the general case.
A Tarski monster group equipped with a non-discrete Hausdorff group topology is a minimal topological group in this sense, since all its proper subgroups are finite (hence discrete in any Hausdorff group topology). Such topologizable Tarski monsters exist by a theorem of Klyachko, Olshanskii and Osin.
References: - The Kourovka Notebook - A. A. Klyachko, A. Yu. Olshanskii, D. V. Osin, On topologizable and non-topologizable groups, Topology Appl. 160 (2013), 2104–2120, arXiv:1210.7895, Theorem 1.4.
Quoted from FormalConjectures/Kourovka/1_74.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 1 open and 1 solved.
Kourovka.«1.74».kourovka_1_74
Open: stated without proof.
Describe all minimal topological groups, that is, all non-discrete Hausdorff topological groups whose proper closed subgroups are all discrete.
theorem kourovka_1_74 :
∀ (G : Type) [Group G] [TopologicalSpace G],
IsMinimalTopologicalGroup G ↔
kourovka_1_74.answer G
Category research open; AMS 20 Group theory and generalizations, 22 Topological groups, Lie groups. Declared in FormalConjectures/Kourovka/1_74.lean, line 61.
Kourovka.«1.74».kourovka_1_74.variants.tarski_monster
Solved: stated here without proof.
There exists a Tarski monster group that admits a non-discrete Hausdorff group topology. This follows from Theorem 1.4 of Klyachko, Olshanskii and Osin, which gives a topologizable Tarski monster of every sufficiently large odd exponent \(n\); taking \(n\) to be a prime \(p\) makes every non-trivial proper subgroup cyclic of order \(p\). Any such group is a minimal topological group.
theorem kourovka_1_74.variants.tarski_monster :
∃ (G : Type) (_ : Group G) (_ : TopologicalSpace G),
IsTarskiMonster G ∧ IsTopologicalGroup G ∧ T2Space G ∧
¬ DiscreteTopology G
Category research solved; AMS 20 Group theory and generalizations, 22 Topological groups, Lie groups. Declared in FormalConjectures/Kourovka/1_74.lean, line 83.
Sources
TheoremConjecture 8.8#
by R. I. Grigorchuk
Both parts of the problem are due to D. V. Anosov.
Reference: The Kourovka Notebook
Quoted from FormalConjectures/Kourovka/8_8.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 1 open and 1 solved.
Kourovka.«8.8».kourovka_8_8a
Solved: stated here without proof.
Does there exist a non-cyclic finitely-generated group \(G\) containing an element \(a\) such that every element of \(G\) is conjugate to a power of \(a\)?
Here a power of \(a\) means \(a^n\) for some \(n \in \mathbb{Z}\).
Answered affirmatively by V. S. Guba, Math. USSR-Izv. 29 (1986), 233–277.
theorem kourovka_8_8a :
∃ (G : Type) (_ : Group G), ¬ IsCyclic G ∧ Group.FG G ∧
∃ a : G, ∀ g : G, ∃ n : ℤ, IsConj g (a ^ n)
Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Kourovka/8_8.lean, line 44.
Kourovka.«8.8».kourovka_8_8b
Open: stated without proof.
Does there exist a non-cyclic finitely presented group \(G\) which contains an element \(a\) such that each element of \(G\) is conjugate to some power of \(a\)?
Here a power of \(a\) means \(a^n\) for some \(n \in \mathbb{Z}\).
theorem kourovka_8_8b :
∃ (G : Type) (_ : Group G), ¬ IsCyclic G ∧ Group.IsFinitelyPresented G ∧
∃ a : G, ∀ g : G, ∃ n : ℤ, IsConj g (a ^ n)
Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Kourovka/8_8.lean, line 56.
Sources
TheoremConjecture 19.25#
by B. Curtin, G. R. Pourgholi
Reference: The Kourovka Notebook
- [vDJMM26] W. van Doorn, E. Judin, P. Monticone and D. Morrison, On Some Problems from the Kourovka Notebook, arXiv:2607.17477v1, Theorem 4.1.
Quoted from FormalConjectures/Kourovka/19_25.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved.
Kourovka.«19.25».kourovka_19_25
Solved: stated here without proof.
Let \(G\) and \(H\) be finite groups of the same order with \(\sum_{g \in G} \phi(|g|) = \sum_{h \in H} \phi(|h|)\), where \(\phi\) is the Euler totient function. Suppose that \(G\) is simple. Is \(H\) necessarily simple?
The answer is negative by [vDJMM26, Theorem 4.1]. The groups \(G = \operatorname{PSU}(3,3)\) and \(H = C_6 \times S_4 \times (C_7 \rtimes C_6)\) both have order \(6048\) and totient sum \(23984\), but only \(G\) is simple. In the semidirect product, a generator of \(C_6\) acts on \(C_7\) by multiplication by \(3\) modulo \(7\).
theorem kourovka_19_25 :
¬ ∀ (G H : Type) [Group G] [Group H] [Fintype G] [Fintype H],
Fintype.card G = Fintype.card H →
∑ g : G, φ (orderOf g) = ∑ h : H, φ (orderOf h) →
IsSimpleGroup G → IsSimpleGroup H
Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Kourovka/19_25.lean, line 51.
Sources
TheoremConjecture 20.76#
by L. Pyber Reference: The Kourovka Notebook Solution: K. Muliarchyk, Abelian subgroups of finite 2-groups: counterexamples to Problems 20.75 and 20.76, Proposition 6.1. !
Quoted from FormalConjectures/Kourovka/20_76.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved.
Kourovka.«20.76».kourovka_20_76
Solved: stated here without proof.
Let \(G\) be a finite \(p\)-group and assume that all abelian normal subgroups of \(G\) have order at most \(p^k\). Is it true that every abelian subgroup of \(G\) has order at most \(p^{2k}\)?
The answer is no. Muliarchyk's Proposition 6.1 gives a finite \(2\)-group of order \(2^{145}\) whose abelian normal subgroups have order at most \(2^{42}\), but which contains an elementary abelian subgroup of order \(2^{85} > 2^{84}\).
theorem kourovka_20_76 :
¬ (∀ᵉ (p : ℕ) (hp : p.Prime) (G : Type) (_ : Group G) (hg : IsPGroup p G) (_ : Finite G) (k : ℕ)
(h : ∀ H: Subgroup G, H.Normal ∧ IsMulCommutative H → Nat.card H ≤ p ^ k),
(∀ H : Subgroup G, IsMulCommutative H → Nat.card H ≤ p ^ (2 * k)))
Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Kourovka/20_76.lean, line 40.
Sources
TheoremConjecture 21.149#
by A. V. Zenkov
The problem is due to V. M. Kopytov and N. Ya. Medvedev. Its original form asked for an order automorphism of a Dlab group that is not inner (
kourovka_21_149.variants.not_inner). After that form was solved, the problem was revised to the stronger question below [vDJMM, Appendix A]. [GYZ] answered the revised question for order-preserving embeddings and rank-one slope groups.The Notebook does not define Dlab groups. We follow [Dl] and [GYZ]: the Dlab groups with slope group \(H\) are four groups of order automorphisms of \(I = [0, 1]\) and two groups of order automorphisms of the extended real line \(\overline{\mathbb{R}}\). All six are viewed as subgroups of the order automorphisms of \(\mathbb{R}\) (
IsDlabGroup).References: - The Kourovka Notebook, Problem 21.149. The original wording is in arXiv:1401.0300v43. - [GYZ] T. Gong, Y. Yang and M. R. Zeng, An order automorphism of a Dlab group not induced by conjugation, arXiv:2609.18630. - [vDJMM] W. van Doorn, E. Judin, P. Monticone and D. Morrison, arXiv:2607.17477. - [Dl] V. Dlab, On a family of simple ordered groups, J. Austral. Math. Soc. 8 (1968), 591–608.
Quoted from FormalConjectures/Kourovka/21_149.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 2 solved.
Kourovka.«21.149».kourovka_21_149
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/kourovka-21-149-lean/blob/5c34c22661071d412f66a42009a1fe68db473b31/lean/Kourovka21149FC.lean#L5740-L5775.
Are there order automorphisms of Dlab groups that are not induced by conjugation by elements of a (possibly bigger) Dlab group?
A Dlab group \(G\) (on \(I\) or on \(\overline{\mathbb{R}}\)) carries Dlab's order, and \(\alpha\) is an automorphism of \(G\) that preserves it. The automorphism \(\alpha\) is induced by conjugation in a bigger Dlab group \(A\) if \(G\) embeds into \(A\) by an injective homomorphism \(e\) and some \(u \in A\) satisfies \(e(\alpha(f)) = u^{-1} e(f) u\) for all \(f \in G\). This includes the inclusions and the order-preserving embeddings of [GYZ]. The slope groups are arbitrary.
theorem kourovka_21_149 :
∃ (K : Subgroup NNRealˣ) (G : Subgroup (ℝ ≃o ℝ)), IsDlabGroup K G ∧
∃ α : G ≃* G, (∀ f g : G, DlabLt (α f) (α g) ↔ DlabLt f g) ∧
¬ ∃ (H : Subgroup NNRealˣ) (A : Subgroup (ℝ ≃o ℝ)), IsDlabGroup H A ∧
∃ e : G →* A, Function.Injective e ∧ ∃ u : A, ∀ f : G, e (α f) = u⁻¹ * e f * u
Category research solved; AMS 06 Order, lattices, ordered algebraic structures, 20 Group theory and generalizations. Declared in FormalConjectures/Kourovka/21_149.lean, line 105.
Kourovka.«21.149».kourovka_21_149.variants.not_inner
Solved: stated here; a Lean proof is at https://github.com/pitmonticone/Kourovka/blob/dcfdbdad8c434e30f6151fb3b4343364d70eeed4/Kourovka/Problem_21_149.lean#L770-L775; a Lean proof is at https://github.com/KitaKen1/kourovka-21-149-lean/blob/5c34c22661071d412f66a42009a1fe68db473b31/lean/Kourovka21149FC.lean#L5777-L5786.
The original form of the problem: are there order automorphisms of Dlab groups that are not inner automorphisms?
This was answered affirmatively by the formal reasoning agent Aristotle (Harmonic), as reported in [vDJMM, Appendix A].
theorem kourovka_21_149.variants.not_inner :
∃ (K : Subgroup NNRealˣ) (G : Subgroup (ℝ ≃o ℝ)), IsDlabGroup K G ∧
∃ α : G ≃* G, (∀ f g : G, DlabLt (α f) (α g) ↔ DlabLt f g) ∧
¬ ∃ u : G, ∀ f : G, α f = u⁻¹ * f * u
Category research solved; AMS 06 Order, lattices, ordered algebraic structures, 20 Group theory and generalizations. Declared in FormalConjectures/Kourovka/21_149.lean, line 125.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.