---

Claim. Let $s_n$ be the number of subgroups of $S_n$, let $G_r$ be the number of subspaces of $\mathbb{F}_2^{\,r}$, and put $R=\lfloor n/2\rfloor$ and $\varepsilon=n\bmod 2$. Sarid's Theorem 1.3 asserts constants $c,C>0$ and $n_0$ with

$$\left|\frac{s_n}{L_n}-1\right|\leq C\,2^{-cn}\quad(n\geq n_0), \qquad L_n=n!\,G_R\,[y^R]\,(1+y/6)^{\varepsilon}\exp\!\left(\frac{y}{2}+\frac{y^2}{6}+\frac{y^4}{384}\right),$$

where $[y^R]$ extracts the coefficient of $y^R$; the constants are common to both parities. Explicit expansions follow: a saddle-point formula with relative error $O(n^{-1})$ and an elementary formula with four residue-class constants and a first correction of order $n^{-1/4}$ (Section 33). The manuscript Precise asymptotics for subgroups of the symmetric group: the critical model, section capacity, and global reduction (144 pages, file dated 2026-10-02, no printed byline) is posted in the claimant's repository; the claim on the site's proof-claims tab, submitted 2026-10-01 by Amir Sarid as a full proof, names the AI systems ChatGPT 5.6 Sol, ChatGPT 6 Astra and Claude Opus 5.5. Pyber [Py93] had shown $\log s_n\asymp n^2$ and Roney-Dougal and Tracey [RoTr25] that $\log_2 s_n=(1/16+o(1))n^2$; the claim would give the asymptotic formula that Problem 1162 asks for. The claim value is answered because the problem asks for a formula rather than stating an assertion to prove or refute.

Submission note. Posted to erdosproblems.com as a proof claim by Amir Sarid (account aimir) on 1 October 2026, giving "ChatGPT 5.6 Sol, ChatGPT 6 Astra, Claude Opus 5.5" as the AI used:

This work proves a precise asymptotic formula for the number of subgroups of $S_n$, with exponentially small relative error. The formula involves the $\lfloor n/2\rfloor$-th coefficient of an explicit generating function and is therefore rather implicit, but it admits explicit asymptotic expansions with relative error $O(n^{-k})$ for any prescribed $k>0$. I work out two examples: a corrected elementary formula with relative error $O(n^{-1/2})$, and a saddle-point formula with relative error $O(n^{-1})$. While the proof requires substantial finite case analysis, the core idea is that all but an exponentially small proportion of the subgroups are subdirect products of copies of four permutation groups: $C_2\leq S_2$, regular $V_4\leq S_4$, natural $D_8\leq S_4$, and the extraspecial group $2_+^{1+4}\leq S_8$ in its degree-eight action. In odd degree, there is additionally either one fixed point or one natural $S_3$-orbit. Notes: The Lean formalization has an explicit external trust boundary. In particular, it assumes several results from the 2025 Roney-Dougal–Tracey preprint, together with other published bounds and classification and catalogue-completeness results. I plan to formalize as many of these inputs as feasible over the coming weeks. A completely self-contained theorem would require formal proofs of every remaining input. Some of their known proofs depend on CFSG, so closing the trust boundary would require substantial CFSG-dependent formalization, although not necessarily a formalization of the entire CFSG.

The argument. The heart of the argument is that all but an exponentially small share of the subgroups of $S_n$ are assembled, as subdirect products, from copies of four small permutation groups: $C_2$ on two points, the regular Klein four-group $V_4$ on four points, the dihedral group $D_8$ on four points and the extraspecial group $2^{1+4}_+$ on eight points; when $n$ is odd, one further orbit is added, a fixed point or a copy of $S_3$ on three points. Theorem 1.1 counts this critical family as $L_n(1+O(2^{-an}))$, which gives the lower bound. The upper bound rests on a section-capacity theorem for binary permutation modules (Theorem 1.2), quotient-moment estimates on a common source, an exhaustion of the non-binary orbit actions, and weighted recurrences assembled by an induction that establishes boundedness before using it; the manuscript notes that a large finite case analysis is needed, with explicit finite certificates for the bounded cases. In the thread the author explained the coefficient-extraction notation of the abstract and said the manuscript was being simplified, with computational material to move to appendices or external artifacts.

Covers. The asymptotic formula for the number of subgroups of $S_n$, the problem's first question, and not the second question, whether there is a statistical theorem on the orders of the subgroups. The claimant files the claim as a full proof, but the manuscript's abstract and theorems concern the count $s_n$ and its expansions and state no theorem on the distribution of orders, so the page records a partial claim settling the formula question alone.

Formalization. The repository's formal/ directory (Lean 4.30.0) is, by the claimant's own account, conditional on outside results that it takes as hypotheses: several theorems of the 2025 Roney-Dougal and Tracey preprint, bounds from other publications, and results that classify small groups or assert that the group catalogues used are complete; some of the known proofs of these rest on the classification of finite simple groups. At the pinned commit its specification lists the three target statements (exponential relative accuracy, the saddle-point formula and the elementary formula) as targets not yet proved, and its notes state that the GAP and Python computations and file hashes discharge none of the finite obligations in Lean. This corpus has not built or audited the development; it is a formalization link and not formalized evidence.

Standing. Claimed. The site labels the problem OPEN (page last edited 2026-01-23) and marks proof claims as unexamined by anyone associated with it. No review or publication is recorded, and the manuscript is posted only in the claimant's repository. Nothing on this page is independently reviewed by this project.