Erdős Problem 911

### What is the conjecture

https://www.erdosproblems.com/911

Let $\hat{R}(G)$ denote the size Ramsey number, the minimal number of edges $m$ such that there is a graph $H$ with $m$ edges that is Ramsey for $G$.

Is there a function $f$ such that $f(x)/x\to \infty$ as $x\to \infty$ such that, for all large $C$, if $G$ is a graph with $n$ vertices and $e\geq Cn$ edges then
$$\hat{R}(G) > f(C) e?$$

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 911 statement and inspect existing formalized conjectures in the repository for the project's conventions. Determine how this conjecture can be represented in Lean, then add the formal statement and verify it using the repository's available checks.

Written by the indexing model from the issue text.