Dead end: U56 (vary)

Settle Lemma.erdos_108: prove it or disprove it Method: Prove Lemma.erdos_108 or its negation: ∀ r ≥ 4, ∀ k ≥ (2 : ℕ), ∃ (f : ℕ), ∀ (V : Type u) (G : SimpleGraph V) (_ : Nonempty V) (hchro : f ≤ SimpleGraph.chromaticNumber G), ∃ (H : G.Subgraph), (SimpleGraph.girth H.coe ≥ r) ∧ (SimpleGraph.chromaticNumber H.coe ≥ k). Question from Erdős problem 108 (https://www.erdosproblems.com/108): For every r ≥ 4 and k ≥ 2 is there some finite f(k,r) such that every graph of chromatic number ≥ f(k,r) contains a subgraph of girth ≥ r and chromatic number ≥ k? Formal statement: formal-conjectures FormalConjectures/ErdosProblems/108.lean. Start from proofs/Lemma.erdos_108.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the lab's maintainers 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): U56 dead end for Lemma.erdos_108. I checked the elaborated statement with pp.all. r, k and f are all ℕ, and hchro is (f : ℕ∞) ≤ chromaticNumber G. SimpleGraph.girth : SimpleGraph α → ℕ is egirth.toNat, so acyclic H has girth 0 and the condition girth ≥ r ≥ 4 requires H to contain a cycle whose shortest length is ≥ r. That is harmless, because any subgraph with χ ≥ 3 has a cycle, and k = 2 is implied by k = 3. r cannot be ⊤, so there is no forest-based disproof. For infinite G, de Bruijn–Erdős compactness reduces the question to finite subgraphs. The statement therefore matches Erdős problem 108. It is Rödl's theorem for r = 4 (too heavy to formalize in 1h) and open for r ≥ 5. I am submitting the starting files unchanged.

{"proofs":{}}