Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 1021
claims/: The 3 claim pages of Problem 1021, one per claimant's result; the problem's standing derives from them.
Statement. Is it true that, for every , there is a constant such that
where is the bipartite graph between and , with each joined to a unique pair of ?
Status. Proved. The site credits Conlon and Lee [CoLe21], with , and the improvement to by Janzer [Ja19]; both are refereed publications, Conlon--Lee cited from the arXiv v2 manuscript and Janzer from the published six-page paper, and each has a claim page, Conlon and Lee and Janzer, accepted on the refereed venues and the site's credit. The site also credits the case to Erdős [Er64c] and to Bondy and Simonovits [BoSi74]; that case has its accepted partial claim page, Bondy and Simonovits. The proof-claim tab is empty and nothing is independently reviewed here.
Source. erdosproblems.com/1021, accessed 2026-09-04; source keys [Er71, p. 103] and [Er74c, p. 79]. Cite as: T. F. Bloom, Erdős Problem #1021, https://www.erdosproblems.com/1021.
References.
- [BoSi74] Bondy, J. A. and Simonovits, M., Cycles of even length in graphs. J. Combinatorial Theory Ser. B 16 (1974), no. 2, 97-105, doi:10.1016/0095-8956(74)90052-5.
- [CoLe21] Conlon, David and Lee, Joonkyung, On the extremal number of subdivisions. Int. Math. Res. Not. IMRN (2021), 9122-9145.
- [Er64c] Erdős, P., Extremal problems in graph theory. Theory of Graphs and its Applications (Proc. Sympos. Smolenice, 1963) (1964), 29-36.
- [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; p. 103 is one of the site's two source passages for the problem.
- [Er74c] Erdős, Paul, Extremal problems on graphs and hypergraphs. Hypergraph Seminar, Lecture Notes in Math. 411, Springer (1974), 75--84; p. 79 is one of the site's two source passages for the problem. Library home: erdos_1974_extremal_problems_graphs_hypergraphs.
- [Ja19] Janzer, Oliver, Improved bounds for the extremal number of subdivisions. Electron. J. Combin. (2019), Paper No. 3.3, 6.
Formalization. Statement in formal-conjectures.
Current assessment
A primary-source search checked both arXiv records, the publication records and author pages, with targeted correction, recent-subdivision and X-announcement queries. The Conlon--Lee arXiv record lists v2 as the latest version, and Conlon's publication list records [CoLe21]. The Janzer publisher record confirms publication on 5 July 2019, DOI 10.37236/8262. A 2019 Birmingham seminar announcement by Janzer discusses subdivision results; the exact bound here is taken from the published theorem, not the announcement. The same search located Conlon--Janzer--Lee's More on the extremal number of subdivisions; no correction or improved E1021 bound is asserted from it. No primary correction changing the affirmative conclusion was located in this scope. Search silence does not establish that no later correction or quantitative improvement exists, and this page does not claim that the displayed exponent is optimal for every .
The source interfaces rest on Conlon--Lee pp. 1--2, 9 and 14 and Janzer pp. 1--3 and 5--6. The result pages contain precise statements, the graph identification and proof pointers. The intervening dependent-random-choice, regularization and embedding arguments were not fully reconstructed or independently reviewed. Conlon--Lee's published typesetting is not compared with the v2 manuscript; the Janzer text cited is the journal version, not its arXiv v1.
The formal-conjectures file ErdosProblems/1021.lean was added on 19
September 2026
(the file at that commit).
As of that commit it defines as cliqueSubdivision k, the
one-subdivision of , and states two theorems: erdos_1021, the
question with answer True (for every some has
), and erdos_1021.variants.janzer, the
bound with . Both are tagged research solved, and each
carries a formal_proof attribute pointing to the file Erdos1021.lean
of Boris Alexeev's plby/lean-proofs repository, which names Janzer as its
informal author and is a formalization link on the
Janzer
claim page. The community database records a formalized statement (formalized:
yes, last updated 19 September 2026). That Lean was not built or audited here,
so no claim gains formalized evidence.
Progress
The answer is affirmative for the stated graph, with one distinct new vertex for each unordered pair of the original vertices. Indexing that vertex by the pair gives the path . Thus is exactly the one-subdivision of : every edge is replaced by a path of length two, and different edges have different internal vertices. This matches Conlon--Lee's subdivision definition on p. 2 of the arXiv:1807.05008v2 manuscript, dated 8 February 2019, and Janzer's definition on pp. 1--2 of the published six-page paper [Ja19]. The subdivision length is fixed; it is not an arbitrary topological subdivision.
Conlon--Lee's Theorem 5.1 gives the positive exponent gap . Janzer's Theorem 3 improves this to the explicit bound
Hence one may take in the question. The multiplicative constant and any sufficiently-large-order threshold depend on fixed ; no uniform bound for growing with is claimed. The reciprocal of the gap is linear in . The relevant locators are Conlon--Lee, Theorem 5.1 on manuscript p. 9, and Janzer, Theorem 3 on published p. 2.
For comparison, the known probabilistic-deletion lower bound for each fixed and all sufficiently large , with depending only on , is recorded in Janzer, p. 2 and Conlon--Lee, manuscript p. 14, as source context rather than a proof reproduced here.
Known Results
Conlon--Lee's broader Theorem 1.3, on manuscript p. 2, gives for any fixed -free bipartite graph with degree at most two on one side, for some . It applies to : the new-vertex side has degree two, and a four-cycle would require two distinct new vertices adjacent to the same pair of original vertices. The pair-indexed definition rules that out. This is a second direct interface to the question, not an inference from an adjacent even-cycle theorem.
At , , and Janzer's exponent becomes . Janzer p. 2 records the classical tight order for this case; Conlon--Lee p. 9 cites the Bondy--Simonovits upper bound as earlier context. The site's commentary credits Erdős [Er64c] and Bondy and Simonovits [BoSi74] with this case. Bondy and Simonovits's Theorem 1 with gives , so , an accepted partial claim on its claim page; Erdős's [Er64c] statement, given without proof, is disclosed there. The commentary misprints the bound as ; the order is . The [BoSi74] reference and its library digest therefore relate to the cycle case. Even-cycle containment alone does not supply the one-subdivided clique required for every . The Erdős [Er64c] passage is not checked on this page.
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_1974_cycles_even_length_graphs
- conlon_2021_extremal_number_subdivisions
- conlon_2021_extremal_number_subdivisions / theorem_1_3
- conlon_2021_extremal_number_subdivisions / theorem_4_2
- conlon_2021_extremal_number_subdivisions / theorem_5_1
- erdos_1964_extremal_problems_graph_theory
- erdos_1964_extremal_problems_graph_theory / assertion_p33
- erdos_1971_unsolved_problems_graph_theory_combinatorial_analysis
- janzer_2019_improved_bounds_extremal_number_subdivisions
- janzer_2019_improved_bounds_extremal_number_subdivisions / theorem_3
- janzer_2019_improved_bounds_extremal_number_subdivisions / theorem_4