LeinsterGroup.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 5 contain sorry, 0 declared as axioms

Leinster Groups

A finite group is a Leinster group if the sum of the orders of all its normal subgroups equals twice the group's order.

References:

Wikipedia
Leinster, Tom (2001). "Perfect numbers and groups". arXiv:math/0104012

TODO: The following properties from the Wikipedia article can also be formalized:

There are no Leinster groups that are symmetric or alternating.
There is no Leinster group of order p²q² where p, q are primes.
No finite semi-simple group is Leinster.
No p-group can be a Leinster group.
All abelian Leinster groups are cyclic with order equal to a perfect number.

Imports (1)

FormalConjecturesUtil

def LeinsterGroup.IsLeinster A finite group G is a Leinster group if the sum of the orders of all its normal subgroups equals twice the group's order line 48 source
Source documentation
A finite group G is a Leinster group if the sum of the orders of all its normal subgroups equals twice the group's order.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype
Proof uses: Eq, Nat, Finset.sum, Subtype, Subgroup, Subgroup.Normal, Finset.univ, Classical.propDecidable, Nat.card, Membership.mem, HMul.hMul, OfNat.ofNat, Fintype.card
9 instances, coercions and auxiliary constants left out.
```
def IsLeinster (G : Type*) [Group G] [Fintype G] : Prop :=
…
```
theorem LeinsterGroup.infinitely_many_leinster_groups Conjecture: Are there infinitely many Leinster groups? sorry line 61 source
Source documentation
Conjecture: Are there infinitely many Leinster groups?
This asks whether there exist infinitely many (non-isomorphic) finite groups that are Leinster groups.
Formalized via the negation of "Does there exist an n such that all Leinster groups have order less than n".

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, Nat, Group, Fintype, LeinsterGroup.IsLeinster, LT.lt, Fintype.card
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem infinitely_many_leinster_groups : answer(sorry) ↔
    ¬∃ n : ℕ, ∀ G : Type, ∀ (_ : Group G) (_ : Fintype G),
      IsLeinster G → Fintype.card G < n := by
…
```
Mentions: LeinsterGroup.IsLeinster
theorem LeinsterGroup.cyclic_of_perfect_is_leinster Cyclic groups of perfect number order are Leinster groups sorry line 74 source
Source documentation
Cyclic groups of perfect number order are Leinster groups.
This follows from the fact that for a cyclic group, all subgroups are normal and correspond to divisors of the group order, and a number is perfect if and only if the sum of its divisors (including itself) equals twice the number.

depends on sorry what this means
Statement uses: Group, Fintype, IsCyclic, Nat.Perfect, Fintype.card, LeinsterGroup.IsLeinster
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cyclic_of_perfect_is_leinster (G : Type*) [Group G] [Fintype G]
    [IsCyclic G] (h_perfect : Nat.Perfect (Fintype.card G)) :
    IsLeinster G := by
…
```
Mentions: LeinsterGroup.IsLeinster
theorem LeinsterGroup.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 sorry line 86 source
Source documentation
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.

depends on sorry what this means
Statement uses: CommGroup, Fintype, Iff, LeinsterGroup.IsLeinster, And, IsCyclic, Nat.Perfect, Fintype.card
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem abelian_is_leinster_iff_cyclic_perfect (G : Type*) [CommGroup G] [Fintype G] :
    IsLeinster G ↔ IsCyclic G ∧ Nat.Perfect (Fintype.card G) := by
…
```
Mentions: LeinsterGroup.IsLeinster
theorem LeinsterGroup.exists_nonabelian_leinster_group Non-abelian Leinster groups exist sorry line 98 source
Source documentation
Non-abelian Leinster groups exist.
For example, S₃ × C₅ (order 30) and A₅ × C₁₅₁₂₈ are Leinster groups.
Reference: Leinster, Tom (2001). "Perfect numbers and groups".

depends on sorry what this means
Statement uses: Exists, Group, Fintype, And, LeinsterGroup.IsLeinster, Not, Eq, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem exists_nonabelian_leinster_group :
    ∃ G : Type, ∃ (_ : Group G) (_ : Fintype G),
      IsLeinster G ∧ ¬ ∀ (a b : G), a * b = b * a := by
…
```
Mentions: LeinsterGroup.IsLeinster
theorem LeinsterGroup.dihedral_is_leinster_iff_odd_perfect The dihedral group DihedralGroup n (of order 2n) is a Leinster group if and only if n is an odd perfect number sorry line 114 source
Source documentation
The dihedral group DihedralGroup n (of order 2n) is a Leinster group if and only if n is an odd perfect number. This gives a one-to-one correspondence between dihedral Leinster groups and odd perfect numbers.
In particular, the existence of odd perfect numbers is equivalent to the existence of dihedral Leinster groups.
Reference: Leinster, Tom (2001). "Perfect numbers and groups".

depends on sorry what this means
Statement uses: Nat, NeZero, Iff, LeinsterGroup.IsLeinster, DihedralGroup, And, Nat.Perfect, Odd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem dihedral_is_leinster_iff_odd_perfect (n : ℕ) [NeZero n] :
    IsLeinster (DihedralGroup n) ↔ Nat.Perfect n ∧ Odd n := by
…
```
Mentions: LeinsterGroup.IsLeinster