/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilGroup structure via subgroup counts
Reference: arXiv:2604.08040v1 Group Structure via Subgroup Counts by Angsuman Das, Hiranya Kishore Dey, Khyati Sharma (2026)
For a finite group $G$, let $\mathrm{cyc}(G)$ denote the number of cyclic subgroups of $G$, and let $t = \pi(G)$ denote the number of distinct prime divisors of $|G|$.
The paper establishes several structural results of the form "if $\mathrm{cyc}(G)$ or $\mathrm{sub}(G)$ is small relative to $2^t$, then $G$ has a strong structural property":
$\mathrm{cyc}(G) < 5 \cdot 2^{t-2} \implies G$ is nilpotent (Theorem 3.1)
$\mathrm{cyc}(G) < 2^{t+1} \implies G$ is supersolvable (Theorem 4.2)
$\mathrm{sub}(G) < 59 \cdot 2^{t-3} \implies G$ is solvable (Theorem 5.3)
Conjecture 5.5 proposes the analogue for solvability via cyclic subgroup count: if $\mathrm{cyc}(G) < 2^{t+2}$, then $G$ is solvable.
In-Paper Location: Conjecture 5.5, Section 5 "Solvability of a group from $\mathrm{sub}(G)$" (PDF page 15)
OpenConjecture ID: 1512
namespace Arxiv.«2604.08040»variable (G : Type*) [Group G] [Fintype G]
The number of cyclic subgroups of a finite group G.
noncomputable def cyc : ℕ :=
Nat.card {H : Subgroup G // IsCyclic H}
The number of distinct prime divisors of the order of G.
This is $\pi(G)$ in the notation of the paper.
noncomputable def numPrimeFactors : ℕ :=
(Fintype.card G).primeFactors.card
Conjecture 5.5 (Das, Dey, Sharma 2026):
If a finite group G satisfies $\mathrm{cyc}(G) < 2^{t+2}$, where $t = \pi(G)$ is the
number of distinct prime divisors of $|G|$, then G is solvable.
@[category research open, AMS 20]
theorem solvable_of_cyc_lt :
answer(sorry) ↔ ∀ (G : Type) [Group G] [Fintype G],
cyc G < 2 ^ (numPrimeFactors G + 2) → Group.IsSolvable G := ⊢ True ↔ ∀ (G : Type) [inst : Group G] [inst_1 : Fintype G], cyc G < 2 ^ (numPrimeFactors G + 2) → Group.IsSolvable G
All goals completed! 🐙Theorem 3.1. Below $5 \cdot 2^{t-2}$ cyclic subgroups, the group is nilpotent.
@[category research solved, AMS 20]
theorem nilpotent_of_cyc_lt (h : cyc G < 5 * 2 ^ (numPrimeFactors G - 2)) :
Group.IsNilpotent G := G:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:cyc G < 5 * 2 ^ (numPrimeFactors G - 2)⊢ Group.IsNilpotent G
All goals completed! 🐙Theorem 4.2. Below $2^{t+1}$ cyclic subgroups, the group is supersolvable.
Stated here as solvability, which supersolvability implies, since Mathlib does not
currently have a standalone IsSupersolvable class.
@[category research solved, AMS 20]
theorem solvable_of_cyc_lt_two_pow_succ (h : cyc G < 2 ^ (numPrimeFactors G + 1)) :
Group.IsSolvable G := G:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:cyc G < 2 ^ (numPrimeFactors G + 1)⊢ Group.IsSolvable G
All goals completed! 🐙The alternating group on five letters has order $60 = 2^2 \cdot 3 \cdot 5$.
⊢ (Nat.card (Fin 5)).factorial = 2 * 60
All goals completed! 🐙The alternating group on five letters has exactly $32$ cyclic subgroups: the trivial one, $15$ of order $2$, $10$ of order $3$ and $6$ of order $5$.
@[category test, AMS 20]
theorem cyc_alternatingGroup_five : cyc (alternatingGroup (Fin 5)) = 32 := ⊢ cyc ↥(alternatingGroup (Fin 5)) = 32
All goals completed! 🐙$A_5$ is the sharpness witness: it has $\pi(A_5) = 3$ and $\mathrm{cyc}(A_5) = 32 = 2^{3+2}$, so it misses the strict inequality $\mathrm{cyc}(G) < 2^{t+2}$ by exactly $1$. This confirms $A_5$ is consistent with Conjecture 5.5 despite being non-solvable.
⊢ ¬32 < 2 ^ ({2, 3, 5}.card + 2)
All goals completed! 🐙The trivial group has exactly one cyclic subgroup (itself).
⊢ Subsingleton { H // IsCyclic ↥H } ∧ Nonempty { H // IsCyclic ↥H }
All goals completed! 🐙The trivial group has zero prime divisors.
@[category test, AMS 20]
theorem numPrimeFactors_trivial : numPrimeFactors PUnit = 0 := ⊢ numPrimeFactors PUnit.{u_2 + 1} = 0
All goals completed! 🐙end Arxiv.«2604.08040»