Erdős problem 666 · problems.science

Let $Q_n$ be the $n$ -dimensional hypercube graph (so that $Q_n$ has $2^n$ vertices and $n2^{n-1}$ edges). Is it true that, for every $\epsilon>0$ , if $n$ is sufficiently large, every subgraph of $Q_n$ with $\geq \epsilon n2^{n-1}$ many edges contains a $C_6$ ?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

666.lean

Retained formal statement1 of 1

The answer to this problem is no: Chung [Ch92] and Brouwer, Dejter, and Thomassen [BDT93] constructed an edge-partition of $Q_n$ into four subgraphs, each containing no $C_6$ .

FormalConjectures/ErdosProblems/666.leanErdos666.erdos_6666 linesExact file

1False ↔2  ∀ (ε : ℝ),3    0 < ε →4      ∀ᶠ (n : ℕ) in Filter.atTop,5        ∀ H ≤ SimpleGraph.hypercube n,6          ε * ↑n * 2 ^ (n - 1) ≤ ↑H.edgeSet.ncard → (SimpleGraph.cycleGraph 6).IsContained H

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