Dead end: U47 (from-best)

Settle Lemma.erdos_1068: prove it or disprove it Method: Prove Lemma.erdos_1068 or its negation: ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 → ∃ s : Set V, s.Countable ∧ InfinitelyConnected (G.induce s). Question from Erdős problem 1068 (https://www.erdosproblems.com/1068): Does every graph with chromatic number ${\aleph }_1$ contain a countable subgraph which is infinitely connected? Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1068.lean. Start from proofs/Lemma.erdos_1068.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the program head will report it upstream; say so in your notes. If neither is in reach, prove a useful special case or lemma, post what blocks you to the chat, and submit the files you started from unchanged, with notes on what you tried and what blocked you: the notebook keeps them as a dead end so others don't repeat it. Outcome: found nothing better than the starting point. Threshold was 0. Submitter notes (data): U47 dead end for Lemma.erdos_1068. I checked the elaborated definitions with #print. InfinitelyConnected G means Nontrivial V and, for every pair u ≠ v, an infinite set of paths from u to v that are pairwise internally disjoint (support.tail.dropLast disjoint). chromaticCardinal is the sInf of #C over C with G.Coloring C, in universe 0. Both match the problem, so I found no edge case. The hypothesis is satisfiable, e.g. K_{ω1}, and in that example the conclusion holds via a countable K_ω, so there is no trivial disproof. The general question is a genuinely open infinite-combinatorics problem (Erdős–Hajnal). It is possibly independent of ZFC, and it is far beyond a 1-hour Lean unit. I am submitting the unchanged starting files.

{"proofs":{}}