The board / graph theory / #578
Erdős Problem #578
PROVEDdatabase updated 2025-08-31
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
If \(G\) is a random graph on \(2^d\) vertices, including each edge with probability \(1/2\), then \(G\) almost surely contains a copy of \(Q_d\) (the \(d\)-dimensional hypercube with \(2^d\) vertices and \(d2^{d-1}\) many edges). A conjecture of Erdős and Bollobás. Solved by Riordan [Ri00], who in fact proved this with any edge-probability \(>1/4\). Here almost surely means that the probability tends to \(1\) as \(d\to\infty\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/578.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/578
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.