Erdős Problem 837

### What is the conjecture

https://www.erdosproblems.com/837

Let $k\geq 2$ and $A_k\subseteq [0,1]$ be the set of $\alpha$ such that there exists some $\beta(\alpha)>\alpha$ with the property that, if $G_1,G_2,\ldots$ is a sequence of $k$-uniform hypergraphs with
$$\liminf \frac{e(G_n)}{\binom{\lvert G_n\rvert}{k}} >\alpha$$
then there exist subgraphs $H_n\subseteq G_n$ such that $\lvert H_n\rvert \to \infty$ and
$$\liminf \frac{e(H_n)}{\binom{\lvert H_n\rvert}{k}} >\beta,$$
and further that this property does not necessarily hold if $>\alpha$ is replaced by $\geq \alpha$.

What is $A_3$?

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 conjecture statement and the linked description at erdosproblems.com/837, then inspect existing formalized conjectures in this repository for conventions. The work is done when the statement determining A_3 is formalized in Lean and fits the project's validation checks.

Written by the indexing model from the issue text.