Erdős Problem 1175

Reference: erdosproblems.com/1175

Formalization notes

• Chromatic cardinal: SimpleGraph.chromaticCardinal is the cardinal-valued chromatic number defined in FormalConjecturesForMathlib. It extends the finite chromaticNumber (which takes values in ℕ∞) to a Cardinal, and is therefore able to distinguish between different infinite chromatic numbers.
• Triangle-free subgraph: a subgraph H : G.Subgraph is triangle-free when H.coe.CliqueFree 3. This is the standard Mathlib formulation: CliqueFree 3 means the graph has no K₃ as a clique.
• Subgraph: we use G.Subgraph (a spanning subgraph record) rather than an induced subgraph since the problem asks for any subgraph, not just induced ones.

theorem Erdos1175.erdos_1175 : sorry ↔ ∀ (κ : Cardinal.{u_1}), Cardinal.aleph0 < κ → ∃ (μ : Cardinal.{u_1}), ∀ (V : Type u_1) (G : SimpleGraph V), G.chromaticCardinal = μ → ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ

Let $\kappa$ be an uncountable cardinal. Must there exist a cardinal $\lambda$ such that every graph with chromatic number $\lambda$ contains a triangle-free subgraph with chromatic number $\kappa$?

Shelah proved that a negative answer is consistent when $\kappa = \lambda = \aleph_1$ (see erdos_1175.variants.shelah_consistency).

theorem Erdos1175.erdos_1175.variants.shelah_consistency : sorry ↔ ¬∀ (V : Type u_1) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = Cardinal.aleph 1

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.

theorem Erdos1175.erdos_1175.variants.threshold_formulation : sorry ↔ ∀ (κ : Cardinal.{u_1}), Cardinal.aleph0 < κ → ∃ (μ : Cardinal.{u_1}), ∀ (V : Type u_1) (G : SimpleGraph V), μ ≤ G.chromaticCardinal → ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ

Threshold reformulation variant. Replaces chromaticCardinal = λ in the hypothesis of erdos_1175 with λ ≤ chromaticCardinal (a graph of chromatic number ≥ λ has a triangle-free subgraph of chromatic number κ). This is a strengthening of erdos_1175 (see erdos_1175.test.threshold_implies_exact).

theorem Erdos1175.erdos_1175.test.exists_triangle_free_subgraph (V : Type u_1) (G : SimpleGraph V) : ∃ (H : G.Subgraph), H.coe.CliqueFree 3

Every graph has a triangle-free subgraph: the bottom subgraph (with no edges) witnesses triangle-freeness, so the existential ∃ H : G.Subgraph, H.coe.CliqueFree 3 in erdos_1175 is non-vacuous.

theorem Erdos1175.erdos_1175.test.threshold_implies_exact : (∀ (κ : Cardinal.{0}), Cardinal.aleph0 < κ → ∃ (μ : Cardinal.{0}), ∀ (V : Type) (G : SimpleGraph V), μ ≤ G.chromaticCardinal → ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ) → ∀ (κ : Cardinal.{0}), Cardinal.aleph0 < κ → ∃ (μ : Cardinal.{0}), ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = μ → ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ

The threshold variant threshold_formulation is stronger than the exact-equality form erdos_1175: if every graph with chromaticCardinal ≥ μ has the desired triangle-free subgraph, then in particular every graph with chromaticCardinal = μ does too.