Skip to content

Erdős problem 1036

Start work

Let GG be a graph on nn vertices which does not contain a trivial (empty or complete) graph on more than clog⁡nc\log n vertices. Must GG contain at least 2Ωc(n)2^{\Omega_c(n)} many induced subgraphs which are not pairwise isomorphic?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1036.lean

Retained formal statement2 of 3

Alon and Hajnal [AlHa91] proved that GG must contain at least exp⁡(n(log⁡n)−O(log⁡log⁡n))\exp\left(n(\log n)^{-O(\log\log n)}\right) many non-isomorphic induced subgraphs.

FormalConjectures/ErdosProblems/1036.leanErdos1036.erdos_1036.variants.alon_hajnal10 linesExact file
∀ (c : ℝ),  0 < c →    ∃ C,      0 < C ∧        ∀ᶠ (n : ℕ) in Filter.atTop,          ∀ (G : SimpleGraph (Fin n)),            ↑G.cliqueNum ≤ c * Real.log ↑n →              ↑G.indepNum ≤ c * Real.log ↑n →                Erdos1036.HasManyNonIsomorphicInducedSubgraphs G                  (Real.exp (↑n * Real.log ↑n ^ (-(C * Real.log (Real.log ↑n)))))
SolvedStatement only, no proof