---

Claim. Problem 1012 asks how large $n$ must be, in terms of $k\ge0$, for $\binom{n-k-1}2+\binom{k+2}2+1$ edges on $n$ vertices to force a cycle on $n-k$ vertices; the answer is that $n\ge2k+3$ suffices, so $f(k)=2k+3$ is admissible for every $k$, and the edge count cannot be lowered there. The claimed result is D. R. Woodall, Sufficient conditions for circuits in graphs, Proc. London Math. Soc. (3) 24 (1972), no. 4, 739--755 (received 20 August 1970, revised 19 January 1971; issued May 1972, whose nominal first day is this page's date), filed on its card. Its Corollary 11.1 (p. 749), in the corpus's words: a graph on $n\ge r+3$ vertices contains a circuit of every length $d$ with $3\le d\le n-r$ provided it has at least $\binom{n-r-1}2+\binom{r+2}2+1$ edges when $n\ge2r+3$, or at least $[\frac14n^2]+1$ edges when $n<2r+3$. The paper's $r$ is this problem's $k$; the corollary is the case of minimum valency $0$ of Theorem 11 (pp. 747--748), the paper's main theorem. With $r=k$ the first bound is the problem's count and $d=n-k$ lies in the range, which gives the claim. The paper states (p. 749) that the first bound is the least possible because of its graph $G_4(n,r)$, a complete graph on $n-r-1$ vertices and one on $r+2$ vertices sharing a vertex, which has one edge fewer and no circuit of length $n-r$ or more (p. 741); p. 741 records that Erdős asked the question at Oxford in 1969, citing Problem 4 of his 1971 list, and p. 749 presents the corollary as its answer, crediting the cases $r=0$ and $r=1$ to Ore and to Bondy.

How the printed corollary reaches the site's question. The site's $f(k)$ is a threshold, any value from which the implication holds for all larger $n$, and the question asks how small it can be. The corollary gives $f(k)\le2k+3$ directly. For $k+3\le n\le2k+2$ its second bound applies, and the problem's count is at least $[\frac14n^2]+1$ there (with $a=n-k-1$ and $b=k+2$, $a+b=n+1$ and $\binom a2+\binom b2\ge[\frac14n^2]$, an elementary comparison made in this corpus and recorded on the result page as a filing observation, stated by no source), while for $n\le k+2$ the count exceeds $\binom n2$ and the implication is vacuous; so the implication holds for every $n\ge1$, as a thread comment of 29 October 2025 argued from Li and Ning's restatement. Only the first half, $f(k)\le2k+3$ with the sharp count, is Woodall's printed claim; the small range rests on the second bound plus the comparison, and nothing is independently reviewed.

Depends on. Nothing in this wiki; the paper's own statements and the elementary comparison above are the whole argument.

Acceptance. Refereed publication in the Proceedings of the London Mathematical Society (Crossref record: volume s3-24, issue 4, pp. 739--755, issued May 1972), which is the refereed evidence. The reviewed evidence is documented acceptance by named experts and by the site's curator, Thomas Bloom: Li and Ning, Stability of Woodall's theorem and spectral conditions for large cycles, Electron. J. Combin. 30 (2023), P1.39 (refereed, open access; filed on its card), restate the $n\ge2k+3$ half as their Theorem 8 with the same count and range and record that the sharing-vertex graph makes the count sharp, so that the extremal number of $C_{n-k}$ is $\binom{n-k-1}2+\binom{k+2}2$ for $n\ge2k+3$; and the curator labels the problem SOLVED, records Woodall's theorem as settling the question completely, and the community database agrees (it lists the problem as solved as of its last update, 31 October 2025). Read depth: Corollary 11.1 and Theorem 11 are checked clause by clause; the proof of Theorem 11 (pp. 748--749) and the proofs of Lemmas 11.1 and 11.2 and Sublemma 11.2.1 (pp. 745--747) are followed at the level of their case structure, the inequalities not checked, and the cited results of Bondy, Dirac, Pósa and Erdős taken as statements. The earlier cases the site credits, Ore's $f(0)=1$ (Ann. Mat. Pura Appl. 1961, Theorem 4.3) and Bondy's $f(1)=1$ (Discrete Math. 1971, Theorem 2), have their own accepted partial claim pages, Ore 1961 and Bondy 1971, and are special cases of this claim.

Formalization. The file src/latest/ErdosProblems/Erdos1012.lean of Boris Alexeev's repository plby/lean-proofs (3,540 lines at the pinned commit of 2026-09-15, linked above, with the repository's record page ErdosProblems/Erdos1012.md as the record link; first committed 20 August 2026; headed leanprover/lean4:v4.33.0 mathlib v4.33.0; it imports Mathlib modules and sibling developments of the repository for Problems 746 and 916) declares itself "a Lean formalization of a solution to Erdős Problem 1012" and names D. R. Woodall as informal author and Codex and GPT-5.6 Sol as formal authors. Its final theorem erdos_1012 (line 3534) states ∀ k, ValidCutoff k (2 * k + 3), where ValidCutoff k N means that for every $n\ge N$ and every SimpleGraph (Fin n) with at least $\binom{n-k-1}2+\binom{k+2}2+1$ edges (woodallBound n k + 1), the graph has a simple cycle of every length $d$ with $3\le d\le n-k$; the preceding theorem woodall is the same statement for a fixed $n\ge2k+3$, which is the corollary's $n\ge2k+3$ half. The file contains no sorry, axiom or native_decide. It is not built, audited or kernel-checked in this corpus, and no outside examination of it is published, so the page lists no formalized evidence. Neither formal-conjectures nor the community database recorded a formalization of the problem on 2026-10-07.