Erdős Problem 809

### What is the conjecture

https://www.erdosproblems.com/809

Let $k\geq 3$ and define $F_k(n)$ to be the minimal $r$ such that there is a graph $G$ on $n$ vertices with $\lfloor n^2/4\rfloor+1$ many edges such that the edges can be $r$-coloured so that every subgraph isomorphic to $C_{2k+1}$ has no colour repeating on the edges.

Is it true that
$$F_k(n)\sim n^2/8?$$

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 by reading the conjecture and its status at https://www.erdosproblems.com/809, then inspect the repository's existing formalized conjecture statements to determine the expected entry point. Done means adding a Lean formalization of the stated Erdős conjecture, with any appropriate project checks passing.

Written by the indexing model from the issue text.