The board / graph theory / #1067
Erdős Problem #1067
DISPROVED LEANdatabase updated 2026-02-02
The statement as posed is false. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
A graph is infinitely edge-connected if to disconnect the graph requires deleting infinitely many edges. In other words, removing any finite set of edges leaves the graph connected.
Does every graph with chromatic number \(\aleph_1\) contain an infinitely connected subgraph with chromatic number \(\aleph_1\)? Komjáth [Ko13] proved that it is consistent that the answer is no. This was improved by Soukup [So15], who constructed a counterexample using no extra set-theoretical assumptions. A simpler elementary example was given by Bowler and Pitz [BoPi24]. This was formalized in Lean by Alexeev using Aristotle and Aleph Prover.
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/1067.Prizenone
Topicsgraph theory, set theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/1067
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.