Skip to content

Erdős problem 760

The cochromatic number of GG, denoted by ζ(G)\zeta(G), is the minimum number of colours needed to colour the vertices of GG such that each colour class induces either a complete graph or independent set.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

760.lean

Retained formal statement1 of 2

The cochromatic number of GG, denoted by ζ(G)\zeta(G), is the minimum number of colours needed to colour the vertices of GG such that each colour class induces either a complete graph or independent set.

If GG is a graph with chromatic number χ(G)=m\chi(G)=m then must GG contain a subgraph HH with ζ(H)≫mlog⁡m? \zeta(H) \gg \frac{m}{\log m}?

A problem of Erdős and Gimbel, who proved that there must exist a subgraph HH with ζ(H)≫(mlog⁡m)1/2. \zeta(H) \gg \left(\frac{m}{\log m}\right)^{1/2}. The proposed bound would be best possible, as shown by taking GG to be a complete graph.

The answer is yes, proved by Alon, Krivelevich, and Sudakov.

FormalConjectures/ErdosProblems/760.leanErdos760.erdos_7604 linesExact file
True ↔  ∃ c > 0,    ∀ (V : Type u_1) [Finite V] (G : SimpleGraph V) (m : ℕ),      G.chromaticNumber = ↑m → ∃ H k, ↑k ≤ H.coe.cochromaticNumber ∧ c * ↑m / Real.log ↑m ≤ ↑k
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.