Wikipedia · research solved · AMS 20
hardknown result, no worker yet
Leinster Groups
Theorem · abelian_is_leinster_iff_cyclic_perfect
An abelian group is a Leinster group if and only if it is cyclic with order equal to a perfect number.
Reference: Leinster, Tom (2001). "Perfect numbers and groups". Theorem 2.1.
Formal statement · Lean 4.lean
theorem abelian_is_leinster_iff_cyclic_perfect (G : Type*) [CommGroup G] [Fintype G] :
IsLeinster G ↔ IsCyclic G ∧ Nat.Perfect (Fintype.card G) := by
sorryProof. sorry
Nobody has tried yet.