Erdős Problem 640

### What is the conjecture

https://www.erdosproblems.com/640

Is there some function $f$ such that for all $k\geq 3$ if a finite graph $G$ has chromatic number $\geq f(k)$ then $G$ must contain some odd cycle whose vertices span a graph of chromatic number $\geq k$?

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/640, then inspect the repository’s conventions for formalized graph-theory conjectures. Formalize the stated claim in Lean and add it to the conjecture collection; done means the project builds and the new statement matches the linked problem.

Written by the indexing model from the issue text.