Erdős Problem 712 - Turán Numbers of Complete Hypergraphs

### What is the conjecture
See https://www.erdosproblems.com/712

Determine, for any $k>r>2$, the value of $\frac{\text{ex}_r(n,K_k^r)}{\binom nr}$, where $\text{ex}_r(n,K_k^r)$ is the largest number of $r$-edges which can placed on $n$ vertices so that there exists no set of $k$ vertices which is covered by all $\binom kr$ possible $r$-edges.

### Prerequisites needed
blocked on hypergraphs in mathlib https://github.com/leanprover-community/mathlib4/pull/28613

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