---

The claim. Oliver Riordan, Spanning subgraphs of random graphs, Combin. Probab. Comput. 9 (2000), no. 2, 125--148, doi:10.1017/S0963548399004150; the publisher's record gives 1 March 2000 as the online publication date (this page's date) and March 2000 as the issue. The article is not held: the publisher's copy is behind a subscription and no preprint was found in the search. Its abstract, read in the publisher's Crossref record on 2026-09-18 and quoted on the problem page, states that for a random graph $G_p$ on $2^d$ vertices whose edges are chosen independently with a fixed probability $p>1/4$, as $d\to\infty$ $G_p$ almost surely has a spanning subgraph isomorphic to the $d$-dimensional hypercube $Q_d$, answering a question of Bollobás; a stronger result implies that the number of $d$-cubes in $\mathcal G(n,M)$ is asymptotically normally distributed for $M$ in a range, and the method is the second moment method. With $p=1/2>1/4$ this is the problem's statement (probability tending to $1$ as $d\to\infty$), so the claim is full. The theorem's number and page, its exact quantifiers and its proof are not read, since the text is not held.

Acceptance. Refereed: Combinatorics, Probability and Computing is a refereed journal (vol. 9, no. 2, March 2000). Reviewed: the site's curator, Thomas Bloom, labels the problem PROVED and, in the commentary of erdosproblems.com/578 (accessed 2026-10-07; empty discussion thread and proof-claim tab), credits the solution to this paper, noting that it covers every edge probability above $1/4$ and the asymptotic normality of the count of $d$-cubes; the community database records the problem as proved. The Semantic Scholar record lists 91 citing works from 2001 to 2026, whose titles show uses for spanning structures in random graphs and no correction or contrary claim. The acceptance rests on the refereed venue and the site's acceptance together with an abstract identified as such, not on a reading of the theorem; this repository's own review is not claimed as evidence. The earlier partial result of Alon and Füredi (1992), for edge density above $1/2$, is attested only through Chung's 1997 survey, paged at problem_80.

Formalization, not evidence. A public Lean 4 development in Boris Alexeev's lean-proofs repository, Erdos578.lean (linked above at a pinned revision; the file entered the repository on 2026-08-17), declares itself a formalization of a solution to Problem 578 and names Oliver Riordan as its informal author and Codex and GPT-5.6 Sol as its formal authors; its theorem erdos_578 states that the probability that the uniform random graph on $2^d$ labelled vertices contains a spanning $d$-cube tends to $1$, which is the $p=1/2$ statement. The corpus has not built or audited the file, so it gives no formalized evidence and the evidence stays reviewed and refereed.

Depends on. Nothing in this wiki: the proof is the paper's and is not held.