Erdős Problem 576

### What is the conjecture

https://www.erdosproblems.com/576

Let $Q_k$ be the $k$-dimensional hypercube graph (so that $Q_k$ has $2^k$ vertices and $k2^{k-1}$ edges). Determine the behaviour of
$$\mathrm{ex}(n;Q_k).$$

Status: open

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start with the Erdős Problem 576 statement in this issue and inspect existing formalized conjectures in the repository for the expected structure. Determine how the hypercube extremal-graph conjecture should be represented in Lean; done means the conjecture is added consistently with the repository’s formalizations and accepted by its checks.

Written by the indexing model from the issue text.