The board / graph theory / #717
Erdős Problem #717
PROVEDdatabase updated 2025-08-31
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The edges of \(K_r\) on `Fin r`, each written as a pair `(i, j)` with `i < j`.
The vertices of a walk other than its two endpoints.
A subdivision of the complete graph \(K_r\) in `G`: `r` distinct branch vertices, and for each edge `(i, j)` of \(K_r\) a path in `G` from the `i`th to the `j`th branch vertex. The interiors of these paths are pairwise disjoint and contain no branch vertex.
Let \(G\) be a graph on \(n\) vertices with chromatic number \(\chi(G)\) and let \(\sigma(G)\) be the maximal \(k\) such that \(G\) contains a subdivision of \(K_k\). Is it true that \[\chi(G) \ll \frac{n^{1/2}}{\log n}\sigma(G)?\] The answer is yes, proved by Fox, Lee, and Sudakov [FLS13, Theorem 1.1]. We read \(\ll\) as: there is an absolute constant \(C > 0\) with this inequality for all graphs on \(n \geq 2\) vertices (for \(n = 1\), \(\log n = 0\)).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/717.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/717
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.