An $\aleph_1$-chromatic graph on $\aleph_1$ vertices whose finite subgraphs are nearly independent (Erdős #75)
Statement
Is there a graph of chromatic number $\aleph_1$ with $\aleph_1$ vertices such that for all $\epsilon>0$, if $n$ is sufficiently large (depending on $\epsilon$) and $H$ is any subgraph on $n$ vertices, then $H$ contains an independent set of size $>n^{1-\epsilon}$? What about the stronger requirement of an independent set of size $\gg n$ (i.e. $\geq cn$ for some constant $c>0$ independent of $n$)?
Acceptance. FULLY RESOLVES: a proof (machine-checkable Lean/Coq preferred, else a full written proof with all steps) EITHER constructing in ZFC a graph with $\aleph_1$ vertices and chromatic number $\aleph_1$ all of whose sufficiently large $n$-vertex subgraphs have independence number $>n^{1-\epsilon}$ for every fixed $\epsilon>0$ (certifying both the chromatic number and the independence property), OR proving in ZFC that no such graph exists, OR a rigorous independence result showing both answers are consistent with ZFC (with the models/forcings exhibited). The linear-independence variant ($\geq cn$) resolved in either direction is a second full target. Any result conditional on extra axioms (CH, MA, PFA, large cardinals) must be clearly flagged. ADVANCES: resolving the question under an additional axiom; a construction achieving the independence property for some but not all $\epsilon>0$; a proof separating the $n^{1-\epsilon}$ and $\gg n$ variants; a reduction to or from Erdős #74 or #750; or a Lean formalization of the [EHS82] construction for the unrestricted-vertex version. Deliver the proof file (or formalization artifact) with the construction and both certifying arguments.
Background
Conjectured by Erdős, Hajnal, and Szemerédi [EHS82, p.120] and repeated in [Er95, p.11] and [Er95d, p.63]; listed as open on erdosproblems.com/75 (fetched 2026-07-13, status 'open', tagged 'graph theory | chromatic number'). The $\aleph_1$-vertex condition is essential: in [Er95] Erdős asked the question without it, but Bloom notes this was an oversight, since [EHS82] already constructs a graph of chromatic number $\aleph_1$ (on more vertices) with the required finite-subgraph independence property. The problem asks whether uncountable chromatic number is compatible with all finite subgraphs being very sparse in the independence sense — a companion to Erdős #74 (infinite-chromatic graphs whose finite subgraphs are nearly bipartite): both probe how locally sparse a graph of large infinite chromatic number can be. In [Er95d] Erdős offered $1000 for a complete solution to all problems of this type (explicitly including #74), and 'a generous reward for any significant partial results'. See also Erdős #750 (erdosproblems.com/750). A formalized Lean statement exists in Google DeepMind's formal-conjectures repository. The attacker's tools: this is proof-shaped infinite combinatorics — candidate constructions from partition calculus and uncountable graph theory (shift-type graphs on ordinals, ladder-system graphs), analysis of their finite subgraphs, and the live possibility that the answer is independent of ZFC, which would require forcing/consistency arguments; the statement and any partial results are natural Lean formalization targets.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #75 (T. F. Bloom) | website |
| REF-02 | Formalized statement of Erdős #75 (Lean, formal-conjectures) | website |
| REF-03 | Erdős Problem #74 (companion problem: nearly-bipartite finite subgraphs) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.