Determine m(n): minimum n-uniform hypergraph without Property B for n ≥ 5

### What is the conjecture

A collection $\mathcal{C}$ of subsets of a finite set has **Property B** if the set can be 2-colored such that every set in $\mathcal{C}$ contains at least one vertex of each color (i.e., no set is monochromatic).

Let $m(n)$ denote the minimum number of sets in an $n$-uniform hypergraph (where all sets have exactly $n$ elements) such that the collection does **not** have Property B.

**Known values:**
- $m(1) = 1$
- $m(2) = 3$
- $m(3) = 7$
- $m(4) = 23$

**Current bounds for $m(5)$:** $29 \leq m(5) \leq 51$

**The problem:** Determine the exact value of $m(n)$ for $n \geq 5$, or derive asymptotically tight bounds. Erdős and Lovász conjectured that $m(n) = \Theta(2^n \cdot n)$.

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

**Sources:**
- https://en.wikipedia.org/wiki/Property_B, https://mathweb.ucsd.edu/~erdosproblems/erdos/newproblems/PropertyB.html, https://link.springer.com/article/10.1007/s10958-022-05828-6, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.31, https://arxiv.org/pdf/2106.13733

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Hypergraph and coloring definitions from `SimpleGraph.Coloring` (existing in FormalConjecturesForMathlib)
- Set systems and uniformity constraints

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of Property B for hypergraphs (2-coloring with bichromatic property)
- Definition and theory of m(n) as the minimum cardinality threshold

Rating justification: Hypergraph coloring and set-theoretic concepts are available in Mathlib/FormalConjecturesForMathlib, but Property B and the m(n) function would require new definitions and supporting lemmas about uniform set systems. The statement itself can be formulated with moderate additional infrastructure.

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

* ams-05
* ams-90

### 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 reading SimpleGraph.Coloring and existing set-system formalizations in FormalConjecturesForMathlib. Determine the precise definitions needed for Property B and the minimum cardinality threshold before choosing a formal statement. Done means the conjecture for n ≥ 5 is added with supporting definitions and lemmas, but the issue does not identify files or tests.

Written by the indexing model from the issue text.