Combinatorics

Erdős problem 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?

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«108»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos108.erdos_108" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ r ≥ 4,
    ∀ k ≥ 2,
      ∃ f,
        ∀ (V : Type u) (G : SimpleGraph V),
          Nonempty V → ↑f ≤ G.chromaticNumber → ∃ H, H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ ↑k

Original conjecture source: FormalConjectures/ErdosProblems/108.lean

Source type SHA-256: sha256:8be2c005c0290f01e2370d1ab68e8a1901ef0b52836b2685bb0fe2075b318142
Task id: fc-v2-erdos108-erdos-108-5e1606f630e799225f5186d6-formalized
Task commitment: sha256:b9fcaaec52f44336854625f37bd694369c962cffb86e90cec18a3e07f098ff2c

References

erdosproblems.com/108

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

True ↔ ∀ r ≥ 4, ∀ k ≥ 2, ∃ f, ∀ (V : Type u) (G : SimpleGraph V), Nonempty V → ↑f ≤ G.chromaticNumber → ∃ H, H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ ↑k