Skip to content

Erdős problem 666

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

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/666.lean

Formal Conjectures

FormalConjectures/ErdosProblems/666.leanErdos666.erdos_6666 linesExact file
False ↔  ∀ (ε : ℝ),    0 < ε →      ∀ᶠ (n : ℕ) in Filter.atTop,        ∀ H ≤ SimpleGraph.hypercube n,          ε * ↑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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:666
  • PLBY Lean proofsErdosProblems.Erdos666

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page