Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 666

claims/: The 2 claim pages of Problem 666, one per claimant's result; the problem's standing derives from them.

Statement. 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$ ?

Status. DISPROVED (LEAN). The site answers the question with no and credits Chung [Ch92] and Brouwer, Dejter and Thomassen [BDT93] with an edge-partition of $Q_n$ into four subgraphs none containing a $C_6$ , so a class with a quarter of the edges avoids $C_6$ ; each paper is recorded as an accepted claim, on the refereed venue and the site's acceptance, on Chung's claim page and the Brouwer--Dejter--Thomassen claim page, from which the frontmatter standing is derived. The site's label is "DISPROVED (LEAN)"; the formalization its Lean qualification refers to is linked on both claim pages and described under Formalization below.

Source. erdosproblems.com/666, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #666, https://www.erdosproblems.com/666.

References.

[BDT93] Brouwer, A. E. and Dejter, I. J. and Thomassen, C., Highly symmetric subgraphs of hypercubes. J. Algebraic Combin. 2 (1993), 25-29.
[Ch92] Chung, Fan R. K., Subgraphs of a hypercube containing no small even cycles. J. Graph Theory (1992), 273-286.
[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.

Formalization. A Lean 4 file in Boris Alexeev's lean-proofs repository, with Aristotle and Alexeev as its formal authors, proves the negation of the statement from the four-part partition and names Chung and Brouwer, Dejter and Thomassen as its informal authors; Alexeev reported it on the site's thread on 6 February 2026. It is a formalization link on both claim pages; the corpus has not built or audited it, so it gives no formalized evidence. The formal-conjectures statement file, tagged research solved, names the lean-proofs development as its formal proof; it states the problem and is not itself a formalization of a result.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (11)

Chung's hexagon-free subgraphs of the hypercube with a quarter of the edges Brouwer, Dejter and Thomassen's four-coloring of the hypercube without monochromatic quadrangles or hexagons problems/extremal_graph_theory/E0666/claims Extremal and Structural Graph Theory extremal_graph_theory/baber_2012_turan_densities_hypercubes Theorem 3.1 (p. 8): edge Turán densities of Q_2 and C_6, first bounds Theorem 4.1 (p. 9): edge Turán densities of Q_2 and C_6 via partial hypercubes extremal_graph_theory/balogh_2014_upper_bounds_cycle_free_subgraphs_hypercube Theorem 2 (p. 2): the 6-cycle Turán density of the hypercube is at most 0.3755 extremal_graph_theory/brouwer_1993_highly_symmetric_subgraphs_hypercubes Section 3 (p. 28): a four-coloring of the n-cube's edges with no monochromatic quadrangle or hexagon, and Erdős's hexagon conjecture false for ε ≤ 1/4

Graph