The board / graph theory / #737
Erdős Problem #737
PROVEDdatabase updated 2025-10-01
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` has chromatic number exactly \(\aleph_1\): it has a proper colouring by the countable ordinals (a set of cardinality \(\aleph_1\)) but no proper colouring by `ℕ`.
`G` contains a cycle of length `n` that contains the edge `e`.
Let \(G\) be a graph with chromatic number \(\aleph_1\). Must there exist an edge \(e\) such that, for all large \(n\), \(G\) contains a cycle of length \(n\) containing \(e\)? The answer is yes, proved by Thomassen [Th83]. Erdős, Hajnal, and Shelah [EHS74] proved that \(G\) must contain all sufficiently large cycles (see Erdős Problem 594).
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/737.Prizenone
Topicsgraph theory, chromatic number
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/737
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.