The board / graph theory / #842
Erdős Problem #842
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).
`G` is a graph on `3n` vertices formed by taking `n` vertex-disjoint triangles `T` and adding a Hamiltonian cycle `C` (with all new edges): `G = T ⊔ C` with `T` and `C` edge-disjoint.
Let \(G\) be a graph on \(3n\) vertices formed by taking \(n\) vertex disjoint triangles and adding a Hamiltonian cycle (with all new edges) between these vertices. Does \(G\) have chromatic number at most \(3\)? The answer is yes, proved by Fleischner and Stiebitz [FlSt92].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/842.Prizenone
Topicsgraph theory, chromatic number
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/842
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.