Erdős Problem 81: Partition of chordal graphs into cliques.

### What is the conjecture

https://www.erdosproblems.com/81

Let $G$ be a chordal graph on $n$ vertices - that is, $G$ has no induced cycles of length greater than $3$. Can the edges of $G$ be partitioned into $n^2/6+O(n)$ many cliques?

### Prerequisites needed
Definition of `chordal` seems to be missing in Mathlib.

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