Erdős problem 1036 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1036.lean

Retained formal statement1 of 3

This is true, and was proved by Shelah [Sh98].

FormalConjectures/ErdosProblems/1036.leanErdos1036.erdos_10369 linesExact file

1True ↔2  ∀ (c : ℝ),3    0 < c →4      ∃ δ,5        0 < δ ∧6          ∀ᶠ (n : ℕ) in Filter.atTop,7            ∀ (G : SimpleGraph (Fin n)),8              ↑G.cliqueNum ≤ c * Real.log ↑n →9                ↑G.indepNum ≤ c * Real.log ↑n → Erdos1036.HasManyNonIsomorphicInducedSubgraphs G (2 ^ (δ * ↑n))

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.

Sources

Search problems.science