Erdős Problem 1160: Group Order Conjecture

### What is the conjecture

Let $g(n)$ denote the number of (non-isomorphic) groups of order $n$. The conjecture states: for all positive integers $n$ and $m$, if $n \leq 2^m$ then $g(n) \leq g(2^m)$. Equivalently: the maximum number of non-isomorphic groups attainable for any order $n$ not exceeding $2^m$ does not exceed the number of non-isomorphic groups of order $2^m$ itself.

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

**Sources:**
- https://www.erdosproblems.com/1160, https://en.wikipedia.org/wiki/Enumeration_of_groups (group counting), Blackburn, N., Neumann, P. M., & Venkataraman, G. (2007). The Kourovka Notebook (research problem compilation)

### Prerequisites needed

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

Building blocks (1-3; from search results):
- `Fintype` and `Group` (group theory foundations in Mathlib)
- Equivalence relations and quotient types (for isomorphism classes)

Missing pieces (exactly 2; unclear/absent from search results):
- Definition of $g(n)$ as a function counting isomorphism classes of groups of order $n$
- Infrastructure for enumerating/counting non-isomorphic groups of a given finite order

Rating justification (1-2 sentences): The fundamental group theory concepts exist in Mathlib, but formalizing the enumeration function $g(n)$ and reasoning about it requires new definitions for partitioning groups by isomorphism class and establishing a counting function, which is non-trivial set-up work but does not require deep new mathematical infrastructure.

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

* ams-20

### 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)

Start by reviewing the stated conjecture and the referenced sources, then inspect the existing Fintype, Group, equivalence-relation, and quotient-type infrastructure in the repository. Define what is needed for g(n) and its group isomorphism classes; done means the conjecture is formally stated with the required enumeration infrastructure and verified by Lean.

Written by the indexing model from the issue text.