Erdős Problem 1162: Asymptotic Formula for Number of Subgroups of $S_n$

### What is the conjecture

Let $f(n)$ denote the number of subgroups of the symmetric group $S_n$. The problem asks for an asymptotic formula for $f(n)$ as $n \to \infty$.

**Known Result:** Pyber (1993) proved that $\log f(n) \asymp n^2$. Roney-Dougal and Tracey (2025) refined this to $\log f(n) = \left(\frac{1}{16} + o(1)\right) n^2$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1162, https://en.wikipedia.org/wiki/Symmetric_group

### Prerequisites needed

**Formalizability Rating:** 2/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- `Fintype.card (Subgroup (Equiv.Perm α))` for counting subgroups of symmetric groups
- `Nat.log` or asymptotics notation for expressing growth rates
- Asymptotic analysis framework

Missing pieces (exactly 2; unclear/absent from search results):
- Explicit computation infrastructure for subgroup counting in $S_n$
- Formalized asymptotic equivalence notation and lemmas for statements like $\log f(n) = (\frac{1}{16} + o(1))n^2$

Rating justification (1-2 sentences): The basic mathematical objects (symmetric groups, subgroups, cardinality) exist in Mathlib, so the statement can be expressed. However, developing the asymptotic analysis framework and formalization of $o(1)$ notation for this specific problem would require additional definitions and helper lemmas.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-20
* ams-05

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)