Erdős problem 1175

Shelah's consistency result: it is consistent with ZFC that there exists a graph $G$ with chromatic number $\aleph_1$ such that every triangle-free subgraph of $G$ has chromatic number strictly less than $\aleph_1$.

This shows that a negative answer to Problem 1175 (with $\kappa = \lambda = \aleph_1$) is consistent, so the main statement erdos_1175 is not provable in ZFC.

Formalization caveat (consistency placeholder). Shelah's result is a *consistency* statement — it asserts the existence of a model of ZFC, not a ZFC theorem. Lean operates inside a single (fixed) model of its set theory, so we cannot directly express "consistent with ZFC" without leaving ZFC. Rather than pretend that Shelah's theorem is a bare ZFC negation, we record it here as an explicit answer(sorry) consistency placeholder: the intended conjecture is the model-theoretic statement, and any concrete formalisation must either appeal to an explicit extra axiom (such as Shelah's specific forcing extension) or to a meta-theoretic consistency proof. Until such a wrapper exists in FormalConjectures, we leave the body as sorry.