---

Claim. The edges of the hypercube $Q_n$ can be partitioned into four classes none of which contains a cycle of length $6$. Since $Q_n$ has $n2^{n-1}$ edges, one class has at least $n2^{n-1}/4$ of them, so for every $\epsilon\le1/4$ and every $n$ there is a subgraph of $Q_n$ with at least $\epsilon n2^{n-1}$ edges and no $C_6$, and the statement of Problem 666 is false; the claim is full. The site's commentary credits the partition to F. R. K. Chung, Subgraphs of a hypercube containing no small even cycles, J. Graph Theory 16 (1992), no. 3, 273--286, issued in July 1992 (the day is not recorded, and this page's date is the first of that month), and to the paper of Brouwer, Dejter and Thomassen recorded on its own claim page, whose remark added in proof says that Chung's paper "also solves Erdős' conjecture" (p. 28). Chung's paper is not held in this corpus; its title indicates further results on other short even cycles, which this page does not record.

Acceptance. Refereed: the Journal of Graph Theory is a refereed journal, and the paper is its version of record. Reviewed: T. F. Bloom, the site's curator, who took no part in the paper, labels the problem DISPROVED (LEAN), answers the question with no, and credits Chung's paper and the Brouwer--Dejter--Thomassen paper with the four-part partition (snapshot of 2026-09-05; the thread's one comment reports the Lean formalization described below, and the proof-claims tab is empty). No reading of Chung's argument is recorded in this repository.

Formalization. The file src/latest/ErdosProblems/Erdos666.lean of Boris Alexeev's lean-proofs repository, linked above at a pinned commit, declares itself a formalization of this partition: its header names Chung and Brouwer, Dejter and Thomassen as informal authors and Aristotle and Boris Alexeev as formal authors. It proves not_erdos_666, the negation of the problem's statement for the graph on Fin n → ZMod 2 with adjacency at Hamming distance one, by defining four edge classes from two parities of the lower endpoint's coordinates below and above the edge's direction, proving that they partition the edges and that none contains a six-cycle, and closing by pigeonhole at $\epsilon=1/4$. Alexeev reported the formalization in a comment of 6 February 2026 on the site's thread, linking the repository's record page, which offers the file for five Mathlib versions; the site's Lean qualification refers to it. The file contains no sorry, and a trailing comment reports the axioms propext, Classical.choice and Quot.sound, which is the file's own report. The corpus has not built or audited it, so it supplies no formalized evidence and is not evidence for this page. The formal-conjectures statement erdos_666, tagged research solved, names a copy of this file in the lean-proofs repository as its formal proof; it is a statement file, not a formalization.

Depends on. Nothing in this wiki: the construction is the paper's.