---

Claim. The answer to Problem 71 is yes: for every infinite arithmetic progression $P$ containing even numbers there is a constant $c=c(P)$ such that every graph with average degree at least $c$ contains a cycle whose length lies in $P$. The claimed result is Béla Bollobás, Cycles modulo $k$, Bull. London Math. Soc. 9 (1977), no. 1, 97--98 (received 24 March 1976, revised 9 July 1976); the publisher's online copy shows only its first page, and a scan of both pages is linked from the site's forum thread. The note opens by stating the conjecture of Burr and Erdős it proves: for every odd $k$ there is a constant $c_k$ such that for every $l$ every graph of order $n$ with at least $c_kn$ edges contains a cycle of length $l$ modulo $k$, with $c_k=k^{-1}((k+1)^k-1)$. Theorem 1 (p. 97) and Theorem $1'$ (p. 98) are the engine. Theorem $1'$: a graph of minimum degree at least $(d^s-1)/(d-1)$, $d\ge2$, contains a vertex $x_0$, a path $P$ avoiding it and $d$ paths of length $s$ from $x_0$ to $P$, each meeting $P$ in one vertex and pairwise meeting only in $P$ and $x_0$; Theorem 1, under the stronger bound $(d^s-1)/(d-1)+d-1$, makes the paths pairwise meet only in $x_0$. Theorem 2 (p. 98): for odd $k\ge3$, if $\delta(G)\ge((k+1)^k-1)/k$ or $e(G)\ge((k+1)^k-k-1)n/k$, then $G$ contains a cycle of length $l$ modulo $k$ for every natural number $l$. The proof takes $d=k+1$ and $1\le s\le k$: two of the $k+1$ endpoints on $P$ are at a distance divisible by $k$, and the two paths through $x_0$ close with that segment to a cycle of length $2s$ plus a multiple of $k$; the residues $2,4,\dots,2k$ exhaust $\mathbb Z/k$ for odd $k$.

How the printed theorem reaches the site's question. A progression $P=\{a+md\}$ with an even member has $d$ odd, or $d$ even and $a$ even. For $d$ odd Theorem 2 gives a cycle of length $a$ modulo $d$, but not one of length at least $a$, so the length need not lie in $P$ when $a>d$; placing it in $P$ needs a fan with $2s\equiv a$ modulo $d$ and $2s\ge a$, which Theorem $1'$ supplies at a minimum degree depending on $a$ as well as $d$. For $d$ even Theorem 2 as printed says nothing; the same construction with $s=a/2$ gives a cycle of length $a$ plus a multiple of $d$, since the argument never uses the parity of $k$ before the final residue count. The note's closing paragraph remarks that for even $k$ the bipartite graphs rule out a linear bound for odd residues, which is why the question asks for progressions with even members. Both reductions are the ones the 2026 Lean formalization below carries out in its lemma erdos_71_of_edge_density; this corpus has checked them for the residue count only. The site's label and the formal-conjectures docstring credit the full statement to this paper; Erdős's 1982 report (card, Chapter III, §5, printed p. 71) states the Burr--Erdős conjecture for odd $k$ and every residue $\ell$, as the note does, and credits Bollobás with its proof, writing the constant as $k(k+1)2^k$.

Acceptance. Refereed publication in the Bulletin of the London Mathematical Society (Crossref record, accessed: volume 9, issue 1, pp. 97--98, issued March 1977; the day is the issue's nominal first day, used for this page's date). The site's curator, Thomas Bloom, labels the problem proved and credits this paper, which is the reviewed evidence listed; Erdős reported the proof in 1982. The publisher's online copy omits the note's second page, as the forum thread records (posts of 24 and 25 February 2026), and a forum user posted a scan of both pages there; the site's proof-claim tab is empty. Read depth: the statements above (the conjecture paragraph, Theorems 1, $1'$ and 2 and the closing paragraph) are checked against the scan; the proofs of Theorems 1 and 2 are checked for the residue count only.

Formalization. The file problems/71/Erdos71.lean of Jayyhk/erdos-lean (Lean v4.28.0; 4,717 lines at the pinned commit of 2026-08-05, first added 2026-06-11) declares itself a formalization of Bollobás's argument and proves Erdos71.erdos_71: for every set P : Set ℕ that is an infinite arithmetic progression (P.IsAPOfLength ⊤) with an even member, there is a rational c such that every finite simple graph with averageDegree at least c has a cycle walk whose length lies in P. This is the statement of erdos_71 in the formal-conjectures file for the problem without its answer(True) ↔ wrapper, and that file, at its commit of 2026-09-18, names this proof in its formal_proof attribute. The forum post of 2026-05-24 by the user andresg535 announced the proof as formalized by a mix of AI systems, named in the post as Aristotle, GPT 5.5 and Opus 4.7, and linked an online type-check; the erdos-lean catalog records that post as the proof's source, its state as complete, and its Mathlib revision. The file's roadmap follows Bollobás: an arithmetic lemma that doubling permutes residues modulo an odd $k$, a dense-subgraph lemma, the fan lemma (Theorem $1'$) proved separately for $s=1$, $s=2$ and $s\ge3$, and Theorem 2 for odd moduli. Its main lemma, erdos_71_of_edge_density, then takes a fan with $s=s_0+da$, where $2s_0\equiv a$ modulo $d$, for an odd difference $d\ge3$ (so $2s\equiv a$ and $2s\ge a$); a long cycle for $d=1$; and a fan with $s=a/2$ for an even difference. Its closing comment reports the axioms propext, Classical.choice and Quot.sound. This corpus has not built, replayed or audited the file nor reviewed the fidelity of the Lean statement to the site's question, and no outside examination is published, so the page lists no formalized evidence; the formal-conjectures link and the community database's Lean status (in its record last updated 2026-06-07) are not a documented independent review of the whole statement.