Erdős Problem 1178: Brown-Erdős-Sós Conjecture

### What is the conjecture

For $r \geq 3$ and $e \geq 3$, let $d_r(e)$ denote the minimal number of vertices in an $r$-uniform hypergraph with exactly $e$ edges. The Brown-Erdős-Sós Conjecture asserts that:

$$d_r(e) = (r-2)e + 3$$

In other words, the threshold number of vertices needed in an $r$-uniform hypergraph to guarantee the existence of certain extremal configurations depends linearly on the number of edges, with slope $r-2$ and intercept $3$.

**Known results:** The conjecture is proven for $e = 3$ (Erdős–Frankl–Rödl, 1986), and partial results exist for general $e$; for instance, Sárközy–Selkow (2005) showed an upper bound of $(r-2)e + 2 + \lfloor \log_2 e \rfloor$. The problem remains open for general $r$ and $e$.

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

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

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Finite sets and cardinality (Mathlib.Data.Finset)
- Basic graph/hypergraph definitions could use Mathlib combinatorics

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of $r$-uniform hypergraphs and hypergraph extremal theory not in Mathlib
- Turán-type density notions and extremal hypergraph machinery required

Rating justification: While basic combinatorial objects exist in Mathlib, the specific notions of extremal hypergraph theory (Turán density, $r$-uniform hypergraph families with edge constraints) require significant new theoretical infrastructure. Stating the conjecture requires defining these objects precisely, making this a level-4 task.

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