Erdős Problem 1018

### What is the conjecture

https://www.erdosproblems.com/1018

Let $\epsilon>0$. Is there a constant $C_\epsilon$ such that, for all large $n$, every graph on $n$ vertices with at least $n^{1+\epsilon}$ edges must contain a subgraph on at most $C_\epsilon$ vertices which is non-planar?

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 linked Erdős Problems 1018 statement and inspect existing formalized conjecture entries in this repository. Identify the appropriate Lean entry point and formalization approach; done means the conjecture has been added and the repository's checks pass.

Written by the indexing model from the issue text.