Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 717
claims/: The 1 claim page of Problem 717, one per claimant's result; the problem's standing derives from them.
Statement. Let be a graph on vertices with chromatic number and let be the maximal such that contains a subdivision of . Is it true that
Formulation. The site's wording, accessed 2026-09-19 (the page shows no last-edited date). The question asks for an absolute constant with for every graph on vertices; in the sources' notation, with the maximum of over -vertex graphs, it asks whether . A subdivision of replaces the edges of by internally vertex-disjoint paths; whenever has an edge. Hajós's 1961 conjecture was for every , that is, ; Erdős and Fajtlowicz showed in 1981 that , so the question is whether their counterexamples are of the largest possible order. Erdős's own words are quoted under the Current assessment.
Status. Proved. The answer is yes: Theorem 1.1 of Fox, Lee and Sudakov [FLS13] (Combinatorica 33 (2013), 181--197, refereed; paged from arXiv v3 of 14 February 2012) gives an absolute constant with for , and the paper says suffices, without optimizing it. The order is exact: Theorem 3 of Erdős and Fajtlowicz [ErFa81] (Combinatorica 1 (1981), 141--143, refereed) gives for almost all graphs on vertices, and [FLS13] (p. 2) records the sharper from the random graph at . Acceptance evidence: publication in Combinatorica (per its Crossref record), the credit of the site's curator, Thomas Bloom, and the citing literature found by the search, which contains no dispute. The claim page Fox, Lee and Sudakov 2011 records the result, its scope and its acceptance evidence, from which the frontmatter standing is derived.
Source. erdosproblems.com/717, accessed 2026-09-19: the problem page (PROVED, with the note that the answer is affirmative; no last-edited date shown; source keys [ErFa81], [Er81]; commentary citing [Di52], [Ca74], [ErFa81] and [FLS13]; no formalized statement), its empty discussion thread and its empty proof-claim tab. Cite as: T. F. Bloom, Erdős Problem #717, https://www.erdosproblems.com/717, accessed 2026-09-19.
References.
- [FLS13] Fox, Jacob and Lee, Choongbum and Sudakov, Benny, Chromatic number, clique subdivisions, and the conjectures of Hajós and Erdős-Fajtlowicz. Combinatorica 33 (2013), no. 2, 181--197, doi:10.1007/s00493-013-2853-x (issued April 2013, online 14 June 2013, per the Crossref record; the site's reference text gives the journal, year and pages without the volume). Paged from arXiv:1107.1920v3 (14 February 2012, 14 pp., the latest arXiv version): Theorem 1.1 and Theorem 1.2, p. 2; the deduction, pp. 3--4; Theorem 3.1, p. 4. Library home: fox_2013_chromatic_number_clique_subdivisions_conjectures_hajos; paged at theorem_1_1, theorem_1_2 and theorem_3_1.
- [ErFa81] Erdős, Paul and Fajtlowicz, Siemion, On the conjecture of Hajós. Combinatorica 1 (1981), no. 2, 141--143, doi:10.1007/BF02579269 (June 1981; received 8 June 1979). Theorems 1--3 and the Lemma, p. 142; the closing conjecture, p. 143. Library home: erdos_1981_conjecture_hajos (from the scan in the Erdős archive of the Rényi Institute); paged at theorem_3.
- [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica 1 (1981), no. 1, 25--42, doi:10.1007/BF02579174 (March 1981); Part IV, item 2, p. 8 of the re-typeset copy in the Erdős archive of the Rényi Institute, which has its own pagination. Library home: erdos_1981_combinatorial_problems_which_i_would_most.
- [Ca74] Catlin, Paul A., Subgraphs of graphs. I. Discrete Math. 10 (1974), no. 2, 225--233, doi:10.1016/0012-365X(74)90119-8. Not held; cited for context (Catlin's counterexamples to Hajós's conjecture). [ErFa81] cites Catlin's later paper, Hajós' graph-coloring conjecture: variations and counterexamples, J. Combin. Theory Ser. B 26 (1979), 268--274, for the disproof, as does [FLS13] ("in 1979, Catlin [6] disproved the conjecture for all "); the site's key is the 1974 paper, which Erdős's 1981 paper also cites for it.
- [Di52] Dirac, G. A., A property of -chromatic graphs and some remarks on critical graphs. J. London Math. Soc. 27 (1952), 85--92, doi:10.1112/jlms/s1-27.1.85. Not held; context, the case of Hajós's conjecture, quoted from the site and [FLS13].
Formalization. None. Formal-conjectures had no file
ErdosProblems/717.lean on its main branch on 2026-09-19; the site's page
records no formalized statement; the community database (teorth/erdosproblems,
data/problems.yaml, 2026-09-19) records the problem proved and unformalized,
with no formalized statement (its entry's last update is dated 31 August
2025). A third-party Lean development that declares itself a formalization of
[FLS13], which the catalog does not cite, is linked from the claim page and
described under the Current assessment; this project has not built or audited
it, and it gives no formalized evidence.
Current assessment
The question (the site's formulation, accessed 2026-09-19). The statement above; PROVED, with the note that the answer is affirmative; no last-edited date. The commentary, in this page's words, traces the history: Hajós's original conjecture , settled positively by Dirac [Di52] when and refuted by Catlin [Ca74] whenever ; the much stronger refutation of Erdős and Fajtlowicz [ErFa81], for whom the typical -vertex graph has ; and the affirmative answer, which the site credits to Fox, Lee and Sudakov [FLS13]. The discussion thread has no comments and the proof-claim tab is empty. The community database records the problem as proved (its entry's last update is dated 31 August 2025).
Status support. The status-defining source is Theorem 1.1 of [FLS13] (arXiv v3, p. 2): "There exists an absolute constant such that for ", with "The proof shows that we may take , although we do not try to optimize this constant." The paper names the statement as the conjecture of [ErFa81] ("In [8], Erdős and Fajtlowicz conjectured that this bound is tight up to a constant factor so that . Our first theorem verifies this conjecture."). Theorem 1.1 is deduced on pp. 3--4 by induction on from Theorem 1.2, a two-branch lower bound on , the least over -vertex graphs with independence number at most : when and when with ; Theorem 1.2 is proved (Sections 3--4) with dependent random choice and the Bollobás--Thomason and Komlós--Szemerédi theorem, which the paper quotes as Theorem 3.1 (every graph with vertices and at least edges contains a subdivision of ; Problem 718). Acceptance evidence: Combinatorica is refereed (volume 33, issue 2, April 2013 per the Crossref record); the site's curator, Thomas Bloom, marks the problem proved and credits the paper; none of the twelve citing papers found by the search disputes or sharpens the theorem. Read depth: the statements of Theorems 1.1, 1.2 and 3.1 (pp. 2 and 4) are checked, and the one-page deduction of Theorem 1.1 from Theorem 1.2 was read for structure; the proof of Theorem 1.2 (pp. 4--12) was not read. The journal text is not held and was not compared with the preprint.
The lower bound and the origin. [ErFa81] (p. 141) defines and and announces "there is an absolute constant such that (1) and in fact our proof yields that (1) holds for almost all graphs , i.e. (1) holds true for all but labelled graphs of vertices". Theorem 1 (p. 142): , with and the independence and clique numbers, from the Lemma that a -free graph has ; Theorem 2: arbitrarily large graphs with , from Erdős's 1947 Ramsey bound; Theorem 3: "There is a constant such that for almost all graphs , ", from for almost all graphs and a counting argument giving . The paper closes (p. 143): "We also conjecture that , i.e. that our theorem is best possible apart from the value of the constant." This closing conjecture is the problem's statement in the authors' words. Erdős restates it in [Er81], Part IV, item 2 (copy p. 8): "Let be a labelled graph of vertices its chromatic number and be the size of its largest topologically complete subgraph. The conjecture of Hajós states that ." He then writes for the maximum of over the labelled graphs on vertices (the re-typeset copy prints the display's solidus as "lt"; is ) and continues: "Fajtlowicz and I prove that (1) . In fact we prove that (1) holds for almost all of the graphs . Very likely (1) is best possible i.e. , but this conjecture remains open for the time being". The same passage records Hajós's conjecture as proved for and "recently disproved for by Catlin [16]", and its gloss of a topologically complete graph "or vertices" is the copy's misprint for "of". Read depth: the quoted statements are checked against the texts; the proofs of [ErFa81] were read for structure only.
Adjacent facts (context, not the problem). Dirac's theorem for and Catlin's counterexamples for are quoted from the site, [ErFa81] and [FLS13]; the papers are not held. [FLS13] (p. 2) records that Kühn and Osthus proved Hajós's conjecture for graphs of girth at least 186 and that [ErFa81]'s random-graph example has and ; how behaves between the bounds and that [FLS13] gives (p. 2; the lower bound from the Bollobás--Catlin and Bollobás random-graph results it cites) is not asked by the site and is recorded only as the gap between the proved constants. Problem 718 is the edge threshold for a topological that Theorem 3.1 states.
A third-party Lean formalization (linked, not evidence). Boris Alexeev's
repository plby/lean-proofs, at its commit of 15 September 2026 that the
claim page's links pin, holds src/latest/ErdosProblems/Erdos717.lean (24,673
bytes, 601 lines, with a module folder Erdos717/) and a note
ErdosProblems/Erdos717.md, which presents the file as a formalized proof of
the problem. The header names Fox, Lee and Sudakov as informal authors and
Codex and GPT-5.6 Sol as formal authors, with a second block naming Codex and
a plan file tex/717.tex; it defines a faithful clique-subdivision structure
(distinct branch vertices, paths with pairwise disjoint interiors avoiding the
branch vertices), and the file ends in a #print axioms Erdos717.erdos_717
command; the file contains no sorry. The file declares itself a
formalization of [FLS13], so it is a formalization link on the claim page of
Fox, Lee and Sudakov. Read depth: the header (first 60 lines) and the note;
this project has not built, audited or kernel-checked the file, so the claim
page lists no formalized evidence. The site's page, its label and the
community database do not cite this development.
Search scope. None of the routes below found a dispute of Theorem 1.1, a sharper determination of the constant, or a change of status.
- The site: problem page, discussion thread and proof-claim tab; the
formal-conjectures directory
FormalConjectures/ErdosProblems/(682 entries) and recursive tree (1,751 entries) on main (no file 717); the community database entry (as recorded under Formalization). - arXiv API: the record of 1107.1920 (v3 of 14 February 2012 is the latest;
no journal reference in the record); the search
(abs:"clique subdivision" OR abs:"clique subdivisions" OR abs:Hajos) AND abs:chromaticsorted by date (three records: [FLS13], a 2015 coloring note and a 2009 degree-sequence paper; none on ). - Crossref: the site's DOI form 10.1007/s00493-013-2853-9 has no Crossref record; a bibliographic query returned the article's record under 10.1007/s00493-013-2853-x, which this page cites; the records for [ErFa81], [Er81], [Ca74] and [Di52].
- Semantic Scholar: the citation list of [FLS13] by arXiv identifier (twelve records, titles read: induced subdivisions in graphs of large girth (2026), immersions and Albertson's conjecture, topological minors in typical lifts, dichromatic number and forced subdivisions, clustered variants of Hajós' conjecture, the Kelmans--Seymour conjecture IV, and pseudorandom and sparse-graph papers; none concerns the order of ).
- The primary sources: [FLS13] pp. 1--4 (arXiv v3); [ErFa81] pp. 141--143; [Er81] copy p. 8, with its reference list (pp. 17--18) for [16] and [22].
plby/lean-proofsthrough the GitHub API: the commit of 15 September 2026, the directory listings and the header ofErdos717.lean.
Not searched: MathSciNet, zbMATH, Google Scholar, X. Not held: [Ca74], [Di52], Catlin's 1979 paper, the Bollobás--Catlin and Bollobás papers on and of random graphs, the journal version of [FLS13].
Remaining gaps. (1) Proof coverage: statements only. Theorem 1.1's deduction from Theorem 1.2 was read for structure, the proof of Theorem 1.2 was not read, and [ErFa81]'s half-page proof of Theorem 3 was read for structure; nothing is independently reviewed. (2) The journal version of [FLS13] was not compared with arXiv v3. (3) The sufficient constant is the paper's, not optimal; the true constant is unknown. (4) [Ca74], [Di52] and Catlin's 1979 paper are not held; the history rests on [ErFa81], [FLS13], [Er81] and the site. (5) The third-party Lean development was read as its header only and is linked from the claim page without evidence standing; there is no Lean statement of the problem in the catalog. The Linked library material below is derived from the library links and is not progress.
Known results
- Fox--Lee--Sudakov, Theorem 1.1 (2013, refereed): for , sufficient; the affirmative answer.
- Fox--Lee--Sudakov, Theorem 1.2: the bounds on from which Theorem 1.1 is deduced.
- Erdős--Fajtlowicz, Theorem 3 (1981, refereed): for almost all graphs, with the closing conjecture that this is best possible; the lower bound per [FLS13].
- [Er81], Part IV, item 2 (copy p. 8): the conjecture in Erdős's words, with Hajós's conjecture proved for and disproved for by Catlin.
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.
- erdos_1981_conjecture_hajos
- erdos_1981_conjecture_hajos / conjecture_p143
- erdos_1981_conjecture_hajos / lemma_p142
- erdos_1981_conjecture_hajos / theorem_1
- erdos_1981_conjecture_hajos / theorem_2
- erdos_1981_conjecture_hajos / theorem_3
- fox_2013_chromatic_number_clique_subdivisions_conjectures_hajos
- fox_2013_chromatic_number_clique_subdivisions_conjectures_hajos / theorem_1_1
- fox_2013_chromatic_number_clique_subdivisions_conjectures_hajos / theorem_1_2
- fox_2013_chromatic_number_clique_subdivisions_conjectures_hajos / theorem_3_1
- erdos_1981_combinatorial_problems_which_i_would_most