Combinatorics

Date added 6 Nov 2026

Erdős problem 86

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 every subgraph of

Q_n

with

\geq \left(\frac{1}{2}+o(1)\right)n2^{n-1}

many edges contains a

C_4

$1,024 bounty

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

versions/fc-v2-erdos86-erdos-86-33506d4bddc9b7b36c58768d-formalized →

Formal statement

Proof target

import Mathlib
import FormalConjectures.ErdosProblems.«86»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos86.erdos_86" := by
  sorry

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

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

Original conjecture source: FormalConjectures/ErdosProblems/86.lean

The audit patch changes this file, so the upstream version can differ from the statement above.

Source type SHA-256: sha256:170c3c54690b7337a6efb176e1249c146b925c831c7e1d488178a81f30b3fc7c
Task id: fc-v2-erdos86-erdos-86-33506d4bddc9b7b36c58768d-formalized
Task commitment: sha256:bcb2f2fb7a4a1dd50bcf038d5699349deff3f1f42342eb5ebdbb6b4132de7fa8

References

erdosproblems.com/86

[BHLL14] Balogh, József and Hu, Ping and Lidický, Bernard and Liu, Hong, Upper bounds on the size of 4- and 6-cycle-free subgraphs of the hypercube. European J. Combin. (2014), 75-85.
[BHN95] Brass, Peter and Harborth, Heiko and Nienborg, Hauke, *On the maximum number of edges in a { $C_4$ }-free subgraph of { $Q_n$ }*. J. Graph Theory (1995), 17--23.
[Ba12b] R. Baber, Turán densities of hypercubes. arXiv:1201.3587 (2012).
[Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406.

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord