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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1036.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1036.leanErdos1036.erdos_10369 linesExact file
True ↔  ∀ (c : ℝ),    0 < c →      ∃ δ,        0 < δ ∧          ∀ᶠ (n : ℕ) in Filter.atTop,            ∀ (G : SimpleGraph (Fin n)),              ↑G.cliqueNum ≤ c * Real.log ↑n →                ↑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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1036
  • PLBY Lean proofsErdosProblems.Erdos1036

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry