Erdős Problem 810

### What is the conjecture

https://www.erdosproblems.com/810

Does there exist some $\epsilon>0$ such that, for all sufficiently large $n$, there exists a graph $G$ on $n$ vertices with at least $\epsilon n^2$ many edges such that the edges can be coloured with $n$ colours so that every $C_4$ receives $4$ distinct colours?

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 conjecture statement at erdosproblems.com/810, then inspect existing formalized Erdős problems in this repository to identify the expected entry point and conventions. Done means the conjecture is added as a Lean formalization that matches the repository’s standards and is accepted by the project checks.

Written by the indexing model from the issue text.