Do dense $r$-uniform hypergraphs contain growing subgraphs of density above $r^{-r}$? (Erdős #1075)

Let $r\ge 3$. The conjecture asserts that there exists a constant $c_r>r^{-r}$ such that, for every $\epsilon>0$ and all sufficiently large $n$, the following holds: any $r$-uniform hypergraph on $n$ vertices with at least $(1+\epsilon)(n/r)^r$ edges contains a subgraph on $m$ vertices with at least $c_r m^r$ edges, where $m=m(n)\to\infty$ as $n\to\infty$. In words: exceeding the edge-count threshold $(n/r)^r$ by any constant factor forces a growing subhypergraph whose edge density is bounded strictly above $r^{-r}$.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable Lean/Coq preferred, else a full written proof) that for some fixed $r\ge 3$ (or for all $r\ge 3$) there exists $c_r>r^{-r}$ with the stated growing-subgraph property; OR a disproof exhibiting, for every candidate constant $c>r^{-r}$, an infinite family of hypergraphs just above the threshold $(n/r)^r$ that contain no growing subgraph of density $\ge c$. ADVANCES (each independently checkable): prove the statement for a specific small $r$ (e.g. $r=3$, where $r^{-r}=1/27$) with an explicit constant $c_r>r^{-r}$ and full proof; OR establish, via a flag-algebra / SDP argument, a provable density lower bound strictly improving the trivial $r^{-r}$ toward some $c_r$, with the reproducible numerical certificate; OR give an explicit construction lowering the best-known upper bound on the achievable $c_r$. Deliver the proof, the improved constant plus its certificate, or the extremal construction.