The board / graph theory / #666
Erdős Problem #666
DISPROVED LEANdatabase updated 2026-02-06
The statement as posed is false. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
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\)? 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\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/666.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/666
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.