Erdős Problem 1157: Turán Numbers for Hypergraph Families

### What is the conjecture

For parameters $t, k, r \geq 2$, consider an $r$-uniform hypergraph family $\mathcal{F}$ consisting of all $r$-uniform hypergraphs on $k$ vertices with $s$ edges. The **Turán number** $\mathrm{ex}_r(n, \mathcal{F})$ is the maximum number of edges in an $n$-vertex $r$-uniform hypergraph containing no member of $\mathcal{F}$ as a subhypergraph.

**Brown–Erdős–Sós Conjecture:** For $r > t \geq 2$ and $s \geq 3$, we have
$$\mathrm{ex}_t(n,\mathcal{F}) = o(n^t)$$
whenever $k \geq (r-t)s + t + 1$.

**Known Lower Bound (Brown, Erdős, and Sós):** For all $k > r$ and $s > 1$,
$$\mathrm{ex}_r(n,\mathcal{F}) \gg_{k,s} n^{\frac{rs-k}{s-1}}.$$

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

**Sources:**
- https://www.erdosproblems.com/1157

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Finite sets and set systems (Finset, Set)
- Asymptotic notation ($o(n^t)$ available via Asymptotics)
- Basic combinatorics (cardinality, subsets)

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of $r$-uniform hypergraph families and the Turán extremal number $\mathrm{ex}_r(n, \mathcal{F})$
- Proof infrastructure for the growth-rate bounds and polynomial constraints

Rating justification: The statement uses relatively standard combinatorial objects (finite sets, cardinality comparisons) but requires formalization of specialized Turán number theory. The definitions themselves are straightforward but non-standard in Mathlib, placing this in the "moderate infrastructure" category.

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

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

Start with the Erdős Problems 1157 source and review existing repository formalizations using finite sets, set systems, cardinality, and asymptotic notation. The missing work is to define the hypergraph-family and Turán-number concepts and formalize the stated bounds; done means the conjecture is represented in Lean and the project builds.

Written by the indexing model from the issue text.