therefore
Sign up
Open navigation
All open problems
Source labels openChecked July 26, 2026

Kourovka NotebookGroup theory

Conjecture 19.25: 25»

Let GG and HH be finite groups of the same order with ∑g∈Gϕ(∣g∣)=∑h∈Hϕ(∣h∣)\sum_{g \in G} \phi(|g|) = \sum_{h \in H} \phi(|h|), where ϕ\phi is the Euler totient function. Suppose that GG is simple. Is HH necessarily simple?

Group theoryAMS 20

Mathematical statement

Let GG and HH be finite groups of the same order with ∑g∈Gϕ(∣g∣)=∑h∈Hϕ(∣h∣)\sum_{g \in G} \phi(|g|) = \sum_{h \in H} \phi(|h|), where ϕ\phi is the Euler totient function. Suppose that GG is simple. Is HH necessarily simple?

Statement source: Kourovka Notebook statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

kourovka.«19.25»

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem kourovka.«19.25» : answer(sorry) ↔    ∀ (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 := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References

Pinned Formal Conjectures sourceformalizationThe Kourovka Notebookbackground