Add Erdős Problem 1175 (triangle-free subgraph of uncountable chromatic graph)#3786
Add Erdős Problem 1175 (triangle-free subgraph of uncountable chromatic graph)#3786henrykmichalewski wants to merge 4 commits intogoogle-deepmind:mainfrom
Conversation
…atic graph Formalises Problem 1175 asking whether every graph of uncountable chromatic number has a triangle-free subgraph of uncountable chromatic number. Uses chromaticCardinal from upstream, and records Shelah's consistency result for the negative direction when κ=λ=ℵ₁ together with a threshold reformulation. Reference: https://www.erdosproblems.com/1175 Assisted by Claude (Anthropic).
|
Closes #1998 |
Mirrors the Round C docstring pass from the private repo's phase1-infrastructure branch. Each Lean file now carries the canonical source statement and upstream URL inline so reviewers can verify formalization against the source without navigating away from the diff.
| ∀ (κ : Cardinal), ℵ₀ < κ → | ||
| ∃ (μ : Cardinal), | ||
| ∀ (V : Type*) (G : SimpleGraph V), G.chromaticCardinal = μ → | ||
| ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ κ ≤ H.coe.chromaticCardinal := by |
There was a problem hiding this comment.
Does the source ask for a triangle-free subgraph with chromatic number exactly κ? This conclusion only requires κ ≤ H.coe.chromaticCardinal, which is a weaker/different formulation unless there is a reason to use at least. Could you either use equality or add a note explaining why the ≥ κ version is intended?
| wrapping as a `sorry`. | ||
| -/ | ||
| @[category research solved, AMS 5] | ||
| theorem erdos_1175.variants.shelah_consistency : |
There was a problem hiding this comment.
Should this consistency result be stated as an outright negation in the ambient theory? The prose says Shelah proved consistency of a counterexample, not that ZFC proves this negation. Could you encode the extra model-theoretic or axiom hypothesis explicitly, or keep this as a documented consistency placeholder rather than a bare negation?
Paul-Lez
added
the
awaiting-author
…consistency placeholder (Paul-Lez review) Two fixes per Paul-Lez's review: - The headline used `κ ≤ H.coe.chromaticCardinal`, but the source asks for a triangle-free subgraph with chromatic number EXACTLY κ. Changed to `H.coe.chromaticCardinal = κ` in the headline and in the threshold variant (and the supporting `threshold_implies_exact`). - The Shelah consistency variant was stated as a bare ZFC negation. Wrapped it as `answer(sorry)` and documented that this is a consistency placeholder requiring an extra-axiom or model-theoretic encoding outside ZFC.
|
Thanks for the review @PaulLez. Pushed d305709 on |
2 participants
Formalises Erdős Problem 1175: does every graph of uncountable chromatic number contain a triangle-free subgraph of uncountable chromatic number?
Contents
chromaticCardinalfrom upstream.Assisted by Claude (Anthropic).