Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 1012
claims/: The 3 claim pages of Problem 1012, one per claimant's result; the problem's standing derives from them.
Statement. Let . Let be such that every graph on $n\geq f(k)$ vertices with at least edges contains a cycle on vertices. Determine or estimate .
Formulation. The site's wording as accessed (page last edited 28 December 2025). is a threshold: any for which the implication holds for all , and "determine or estimate" asks how small it can be taken. The edge count is one more than the number of edges of the graph made of a and a sharing one vertex, which has vertices and no cycle on more than vertices when (every cycle lies in one block; an elementary remark, and the statement Woodall [Wo72] makes of this graph, his , on p. 741), so the count cannot be lowered there; at it is Ore's threshold . Erdős's 1971 item 4 prints the count as , with "for " and the request to "determine or estimate "; the site's is his , and the site's count differs from the printed one, which at exceeds and so cannot be what was meant (the site's maintainer agrees in the thread that the printed statement looks wrong even at ); the site's count is the one for which Erdős's "best possible" holds, and it is the count Bondy's 1971 paper [Bo71b], which attributes its case to Erdős at the Oxford conference, prints for the general problem (its at , p. 126). The site labels the problem SOLVED, its label for a resolution that is neither a proof nor a disproof: the question is a determination, answered by a theorem giving .
Status. Solved. Woodall's Corollary 11.1 [Wo72] (Proc. London Math. Soc. (3) 24 (1972), 739--755; printed p. 749): a graph on vertices with at least edges when , or at least edges when , contains a circuit of length for every ; with the first bound is this problem's count and is in range, so works for every , and the paper states (p. 749) that the first bound is the least possible because its , the sharing-vertex graph, has no circuit of length or more. The paper introduces the corollary as the answer to Erdős's 1969 question (pp. 741 and 749, citing Problem 4 of [Er71]). Theorem 8 of Li and Ning [LiNi23] (Electron. J. Combin. 30 (2023), P1.39; refereed, open access; p. 4) restates the half with the same count and range, and records that the sharing-vertex graph shows the count is sharp, "which means that for ". The status rests on the original's statement and the structure of its proof of Theorem 11, with the refereed restatement and the site's account (which records Woodall's theorem as settling the question completely) agreeing. The smallest admissible : the corollary's second bound covers , and this problem's count is at least there (an elementary comparison recorded on the library's result page as a filing observation), so the implication holds for every and is vacuous for , where the count exceeds ; the thread's reading that no fails rests on the printed corollary plus that comparison, and nothing is independently reviewed. The claim page Woodall records the result, its acceptance evidence and its postings, and the standing derives from it. The site also credits Ore [Or61] with (an accepted partial claim, Ore 1961; Theorem 4.3, p. 320, states the threshold with its sharpness, and Erdős's 1962 note quotes it) and Bondy [Bo71b] with (an accepted partial claim, Bondy 1971; Theorem 2, p. 125, states that a graph of order and size at least has a cycle of length , printed without a range for ), and says the existence of follows from Erdős's 1962 theorem [Er62e] by an argument given in the thread (recorded below with its provenance).
Source. erdosproblems.com/1012, accessed 2026-09-18: the problem page (labeled SOLVED, the site's label for a resolution that is neither a proof nor a disproof; last edited 28 December 2025; source keys [Er62e], [Er71, p. 98]; commentary citing [Or61], [Bo71b], [Wo72]), its five-comment discussion thread (17 September to 12 November 2025) and its empty proof-claim tab. Cite as: T. F. Bloom, Erdős Problem #1012, https://www.erdosproblems.com/1012, accessed 2026-09-18.
References.
- [Wo72] Woodall, D. R., Sufficient conditions for circuits in graphs. Proc. London Math. Soc. (3) 24 (1972), no. 4, 739--755, doi:10.1112/plms/s3-24.4.739 (Crossref record: issued May 1972, online at the publisher since December 2016). Corollary 11.1, printed p. 749: a graph on vertices with at least edges when , or edges when , contains a circuit of every length from to ; the case of Theorem 11 (pp. 747--748), whose proof (pp. 748--749) is followed at the level of its case structure. The example and the attribution of the question to Erdős, p. 741. Library home: woodall_1972_sufficient_conditions_circuits_graphs; the corollary is paged at corollary_11_1.
- [LiNi23] Li, Binlong and Ning, Bo, Stability of Woodall's theorem and spectral conditions for large cycles. Electron. J. Combin. 30 (2023), no. 1, Paper No. 1.39, doi:10.37236/11641 (submitted 1 November 2022, accepted 13 February 2023, published 24 February 2023; open access, CC BY-ND). Theorem 8 (Woodall), p. 4; the sharpness sentence and the introduction's survey, pp. 2--3. Filed as li_2023_stability_woodall_theorem_spectral_conditions_large_cycles (a lead used for the attestation; the paper's own results are spectral and not this problem's).
- [Er62e] Erdős, P., Remarks on a paper of Pósa. Magyar Tud. Akad. Mat. Kutató Int. Közl. 7 (1962), 227--229; the Theorem, p. 227. Library home: erdos_1962_remarks_paper_posa (a Rényi archive scan); paged at theorem_p227.
- [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97--109; item 4, p. 98. Library home: erdos_1971_unsolved_problems_graph_theory_combinatorial_analysis (the Rényi archive's scan); the item is paged at item_4.
- [Or61] Ore, Oystein, Arc coverings of graphs. Ann. Mat. Pura Appl. (4) 55 (1961), no. 1, 315--321, doi:10.1007/BF02412090 (Crossref record). Theorem 4.3, printed p. 320: "A graph with edges has a Hamilton circuit. When the only graph without a Hamilton circuit consists of a complete graph, and a single edge connecting it with an outside vertex; in addition, for there is the exceptional graph depicted in Fig. 3." Its proof (pp. 320--321) rests on Ore's 1960 degree theorem, the paper's Theorem 3.2. The statement is the one quoted on p. 227 of [Er62e]: "ORE [2] proved that if then every is Hamiltonian, and he showed that the result is false for ." Library home: ore_1961_arc_coverings_graphs; the theorem is paged at theorem_4_3.
- [Bo71b] Bondy, J. A., Large cycles in graphs. Discrete Math. 1 (1971/72), no. 2, 121--132, doi:10.1016/0012-365X(71)90019-7 (Crossref record; the publisher's open-archive license dated 2013; the article is in the publisher's open archive). Theorem 2, printed p. 125 (PDF p. 5 of the open-archive file): "Let have order and size at least . Then has a cycle of length ", followed by the attribution of the conjecture to Erdős at the Oxford conference of July 1969 and the sharpness graph of complete blocks of orders and ; its proof (p. 127) rests on Ore's theorem, Pósa's degree condition and the theorem of Bondy's pancyclic paper. Conjecture 1 (p. 126), for with , is this problem at , and p. 128 states that it holds for all . [LiNi23] (p. 2) writes that "At almost the same time, some partial result was also obtained by Bondy [4]". Library home: bondy_1971_large_cycles_graphs; the theorem is paged at theorem_2 and the conjecture with its range at conjecture_1.
Formalization. None in the catalogs: formal-conjectures had no file
ErdosProblems/1012.lean on 2026-09-18 (the directory
FormalConjectures/ErdosProblems/ and the recursive tree listed in full)
and none on 2026-10-07; the site's indicator records no formalized
statement; and the community database (teorth/erdosproblems,
data/problems.yaml) records, on 2026-09-18 and on 2026-10-07, the
problem as solved (last update 31 October 2025), unformalized, with no
formalized statement and no OEIS entry. Outside both catalogs, the file
src/latest/ErdosProblems/Erdos1012.lean of Boris Alexeev's repository
plby/lean-proofs (first committed 20 August 2026) declares itself a Lean
formalization of a solution to this problem, names D. R. Woodall as
informal author and Codex and GPT-5.6 Sol as formal authors, and proves
erdos_1012, that is a valid cutoff for every ; it is recorded
as a formalization link on
Woodall's claim page,
which describes the file. The file is not built or audited in this
corpus, so the claim lists no formalized evidence.
Current assessment
The question (site formulation, accessed 2026-09-18). The statement above; SOLVED; last edited 28 December 2025. The commentary, in this page's words, credits four results: Erdős's 1962 paper [Er62e] with the existence of for every , a consequence the paper does not state and which Cambie derives in the thread; Ore [Or61] with , that is, a Hamiltonian cycle in every graph on vertices with at least edges; Bondy [Bo71b] with ; and Woodall [Wo72] with a cycle of every length from to in every graph on vertices with at least edges, which the site says settles the question completely. The thread's five comments are recorded below; the proof-claim tab is empty. The community database lists the problem as solved as of its last update, 31 October 2025.
Status support. Corollary 11.1 of [Wo72] (p. 749; paged at corollary_11_1): a graph on vertices with at least edges when (the paper also writes this condition as ), or at least edges when , contains a circuit of length for every . The paper's is this problem's , and its is a minimum-valency parameter that the corollary sets to ; the corollary is the case of Theorem 11 (pp. 747--748), the paper's main theorem, whose case A1 (, minimum valency at most ) carries the first bound and whose case B1 () carries the second. The sharpness parenthesis (p. 749) says the first bound is the least possible in view of , the complete -gon and complete -gon sharing one vertex, which p. 741 defines for and states to have edges and no circuit of length or more; p. 741 also records the question: "In 1969 Erdös asked whether a graph on vertices, with more edges than , must contain a circuit of length (see [5], Problem 4)", its [5] being [Er71], and p. 749 introduces the corollary as the answer, crediting the case to Theorem 2 of [Bo71b] and the case to Ore [Or61]. So the paper prints this problem's count, with the site's range, as Erdős's question. Theorem 8 of [LiNi23] (p. 4) restates the half: "(Woodall [37]). For a graph of order where is an integer, if , then contains a for each ." Its [37] is [Wo72], and the restatement agrees with the original. The introduction (p. 2) writes: "In the 1970s, Erdős [11] asked how many edges are needed in a graph on vertices, to ensure the existence of a cycle of length exactly . Recall that Woodall [37] proved that for a graph of order where is an integer, if , then contains a for each . At almost the same time, some partial result was also obtained by Bondy [4]", its [11] being [Er71]; and (p. 3), with : "The graph shows Woodall's theorem is sharp, which means that for ." Since is in the range, every graph on vertices with the stated edge count contains a : is admissible for every (and the theorem gives more, every cycle length from to ). Acceptance evidence: [Wo72] is a refereed journal paper (received 20 August 1970, revised 19 January 1971, on its first page; Crossref record), its statement taken as printed, the proof of Theorem 11 followed at the level of its case structure and the lemmas' inequalities not checked; [LiNi23] is a refereed open-access journal paper (submitted, accepted and published dates on its first page; Crossref record) that states the theorem as a theorem of the literature with a citation, and the site's account and the community database agree. The original's statement, numbering and hypotheses are as printed; nothing is independently reviewed. The small range: for the corollary's second bound applies, and this problem's count is at least that (with and , and , smallest when and are as equal as possible; followed in this corpus, a filing observation recorded on the result page), so the count forces a for every , while for the count exceeds and no graph meets the hypothesis. Of the other two named results, Ore's (; a graph on vertices with edges is Hamiltonian, sharp) rests on the original: Theorem 4.3 of [Or61] (p. 320; paged at theorem_4_3) states that edges give a Hamilton circuit and that at edges the only exceptions are with a pendant edge and, for , one further graph; the theorem is printed without a range for , and for its hypothesis cannot be met, so the site's "" holds. The quotation in [Er62e] (p. 227) agrees with it. Bondy's () rests on the original: Theorem 2 of [Bo71b] (p. 125; paged at theorem_2) states that a graph of order and size at least has a cycle of length , and that the graph of complete blocks of orders and , with one edge fewer, has none for ; the theorem is printed without a range for , and for its hypothesis cannot be met while for it is met only by and less an edge, both of which contain a triangle, so the site's "" holds. Its proof (p. 127) is followed at the level the library card states; nothing is independently reviewed. The same paper poses the general question as Conjecture 1 (p. 126): for , where is the least size forcing a cycle of length and ; at this is the site's count and the range of Woodall's theorem. Its § 4 (p. 128) states that Conjecture 1 "holds for all ", that is in the site's letters, an explicit estimate of Erdős's ; the paper proves the equivalence of Conjecture 1 with its circumference form, Conjecture 2 (Corollary 3.2, p. 131), but asserts the range for Conjecture 2 with "we can prove" and a pointer to the method of Theorem 2, without a written proof (paged at conjecture_1). [LiNi23] (p. 2) credits the paper with "some partial result" without saying which, and the paper's closing note (pp. 131--132) points to Woodall's forthcoming paper.
Erdős's 1962 theorem and the existence argument. The Theorem of [Er62e] (p. 227): for and , every graph on vertices with all valencies at least and at least edges is Hamiltonian, and some non-Hamiltonian graph with all valencies at least has edges. The paper contains no statement about cycles of length in any of its three pages, as the site says. The thread (the account StijnC, 14:39 on 17 September 2025) supplies the argument the site refers to: remove from a graph on vertices with no its vertices of minimum degree one at a time; the remaining graph on vertices is non-Hamiltonian, so if its minimum degree is the 1962 theorem gives , the removed vertices contribute at most edges, and for large in terms of the total is maximized at , giving ; the comment treats the case of an isolated vertex in separately and notes the sharpness example. It is recorded on this page as a forum argument with its provenance and is not reproduced as this page's own; the comment adds that "no attempt has been made on an estimate on ".
Erdős's 1971 item 4. [Er71], item 4 (p. 98; paged at item_4): "We proved that every is Hamiltonian and that this is best possible. I showed that for every contains a . My proof is not quite trivial. The result is easily seen to be the best possible. It would be interesting to determine or estimate [6]." The list's [6] is [Er62e]. The printed count is discussed in the Formulation note; the first sentence is Ore's theorem in Erdős's "We proved".
The thread (leads with provenance, not status). Five comments, in this page's words. 17 September 2025, 12:46 (the account StijnC): the commenter could not find the proof in the Rényi copy of [Er62e] and was surprised that the count was not , which at is Ore's correct bound. 17 September 2025, 13:10 (the site's maintainer): the problem is as described in [Er71], problem 4, p. 98, but the maintainer agrees it looks wrong even at ; [Er62e] proves a statement of similar shape that finds a instead, under a minimum degree condition; and the printed statement in [Er71] presumably carries at least one typo. 17 September 2025, 14:39 (StijnC): the existence argument above. 29 October 2025 (StijnC): is known, since the implication holds for every at which it makes sense, so one could say for all ; the comment argues from Woodall's theorem as stated in [LiNi23] (for it takes ); the site was updated. 12 November 2025 (the account Alfaiz): the reference keys [Or61] and [Wo72] failed to display; the site was updated.
Search scope. None of the routes below found a dispute of Woodall's theorem or a later result on the smallest .
- The site: problem page, discussion thread and proof-claim tab; the formal-conjectures directory and tree (no file 1012); the community database entry.
- Crossref: the records of doi:10.1112/plms/s3-24.4.739, doi:10.1016/0012-365X(71)90019-7, doi:10.1007/BF02412090 and doi:10.37236/11641.
- Semantic Scholar: the citation list of [Wo72] (the first 100 of more records, titles and venues only; [LiNi23] among them, with 2024--2026 papers on cycle lengths under minimum-degree conditions and on Turán numbers of long cycles); none disputes the theorem.
- The primary sources: [Er62e] pp. 227--229; [Er71] p. 98; [LiNi23] pp. 1--4 and 18; [Or61] pp. 315--321, [Bo71b] pp. 121--132 and [Wo72] pp. 739--755 (these three accessed).
Not searched: MathSciNet, zbMATH, Google Scholar, X, arXiv (the status-defining sources are pre-arXiv).
Remaining gaps. (1) [Wo72] rests on Corollary 11.1 (p. 749) and Theorem 11 (pp. 747--748) as printed, with 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) followed at the level of their structure; the inequalities are not checked, and the cited results of Bondy, Dirac, Pósa and Erdős that the proof rests on are taken as statements in the paper. (2) [Or61] rests on Theorem 4.3 (p. 320) as printed, with its proof followed; its statement agrees with the quotation in [Er62e]. [Bo71b] rests on Theorem 2 (p. 125) as printed, with its proof followed. Its estimate (p. 128) rests on a step the paper asserts without a written proof and is recorded with that standing. (3) The smallest admissible : Corollary 11.1 of [Wo72] gives every with this problem's count and every with edges; that this problem's count is at least in the small range, and impossible for , is an elementary comparison made in this corpus and recorded on the result page as a filing observation, not a statement of any source. With that standing the implication holds for every , as the thread argued; no source states the small range in this problem's letters. (4) The existence argument from [Er62e] is a forum argument. (5) Proof coverage: the proof of Theorem 11 of [Wo72] followed at the level of its case structure; otherwise statements only. (6) The Lean development in Alexeev's repository (Formalization above) is not built or audited in this corpus.
Known results
- Woodall 1972, Corollary 11.1: for , edges force a circuit of every length from to , and for so do edges; the first bound sharp by , a and a sharing a vertex; , and with the elementary comparison on the result page every ; the case of Theorem 11, the paper's main theorem; agrees with Theorem 8 of [LiNi23].
- Ore 1961, Theorem 4.3: edges force a Hamilton circuit, and at edges the only graphs without one are with a pendant edge and, for , one exceptional graph; (an accepted partial claim, claim page).
- Erdős 1962, Theorem: the minimum-degree Hamiltonicity threshold , with Ore's theorem quoted (: edges, sharp).
- Erdős 1971, item 4: the problem as posed, with the printed edge count and "determine or estimate ".
- Bondy 1971, Theorem 2: edges force a cycle of length , sharp for by and sharing a vertex; printed without a range for ; (an accepted partial claim, claim page).
- Bondy 1971, Conjecture 1: the problem's implication with its sharpness conjectured for all (in the paper's letters for ), and stated on p. 128 to hold for all , the Conjecture 2 half of that range asserted without a written proof; with that standing.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.
- bondy_1971_large_cycles_graphs
- bondy_1971_large_cycles_graphs / conjecture_1
- bondy_1971_large_cycles_graphs / theorem_1
- bondy_1971_large_cycles_graphs / theorem_2
- bondy_1971_large_cycles_graphs / theorem_3
- erdos_1962_remarks_paper_posa
- erdos_1962_remarks_paper_posa / theorem_p227
- erdos_1971_unsolved_problems_graph_theory_combinatorial_analysis
- erdos_1971_unsolved_problems_graph_theory_combinatorial_analysis / item_4
- li_2023_stability_woodall_theorem_spectral_conditions_large_cycles
- li_2023_stability_woodall_theorem_spectral_conditions_large_cycles / theorem_10
- li_2023_stability_woodall_theorem_spectral_conditions_large_cycles / theorem_11
- li_2023_stability_woodall_theorem_spectral_conditions_large_cycles / theorem_7
- li_2023_stability_woodall_theorem_spectral_conditions_large_cycles / theorem_8
- ore_1961_arc_coverings_graphs
- ore_1961_arc_coverings_graphs / theorem_4_1
- ore_1961_arc_coverings_graphs / theorem_4_2
- ore_1961_arc_coverings_graphs / theorem_4_3
- woodall_1972_sufficient_conditions_circuits_graphs
- woodall_1972_sufficient_conditions_circuits_graphs / corollary_11_1
- woodall_1972_sufficient_conditions_circuits_graphs / theorem_11