Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 57

claims/: The 1 claim page of Problem 57, one per claimant's result; the problem's standing derives from them.

Statement. If $G$ is a graph with infinite chromatic number and $a_1<a_2<\cdots $ are lengths of the odd cycles of $G$ then $\sum \frac{1}{a_i}=\infty$ .

Formulation. Here the sequence lists the distinct odd cycle lengths; each length is counted once. Infinite chromatic number means that $G$ is not colorable with any finite number of colors.

Status. The site labels the problem PROVED (LEAN), crediting the solution to Liu and Montgomery; the Lean behind the qualifier is described below. The accepted claim is Liu and Montgomery's odd interval theorem.

Source. T. F. Bloom, Erdős Problem #57, erdosproblems.com/57, accessed 2026-09-05.

References. Original problem references, as listed by the site. [ErHa66], [Er69b], [Er74d], [Er81], [Er90], [Er93, p. 342], [Er94b], [Er95], [Er95d], [Er96], [Er97b], [Va99, 3.58]. These are the site header's historical statement references. Of these, [Er97b] (Erdős, Some old and new problems in various branches of combinatorics, Discrete Math. 165/166 (1997), 227--231) is carded: item 3 on p. 228 states the conjecture, quoted on its card, erdos_1997_some_old_new_problems_various_branches_combinatorics.

Formalization. The formal-conjectures statement file, added on 2026-09-09, states the problem, leaves its proof as sorry and, since 2026-09-18, points through its formal_proof attribute at the Lean development in Boris Alexeev's lean-proofs collection that is linked from the claim page; see Existing formalizations below.

Current assessment

Claims. One claim page, accepted on refereed publication (J. Amer. Math. Soc. 36 (2023)) and on the curator's credit to Liu and Montgomery. It lists no formalized evidence: the Lean development behind the site's qualifier, in Boris Alexeev's lean-proofs collection, declares itself a formalization of Liu and Montgomery's solution and is linked from the claim page, but this corpus has not built it, and Lean outside the corpus's audited set gives no formalized evidence.

Compilation state. The library's pages on the paper record the local deductions from the odd interval theorem to the problem as having passed independent review but identify no separate review report, so that review is not acceptance evidence. The compiled source-proof chain is incomplete at Lemma 3.13’s reservoir compatibility step. Compilation coverage is separate from the problem's standing, which rests on the refereed publication and the curator's credit.

Progress

The site attributes the conjecture to Erdős and Hajnal [ErHa66] and its solution to Liu and Montgomery [LiMo20]. Their Theorem 1.4 proves a stronger finite statement: for every $\varepsilon>0$ and all sufficiently large chromatic numbers $k$ , a graph of chromatic number $k$ contains all odd cycle lengths in some interval $[L,Lk^{1-\varepsilon}]$ . Consequently

\sum_{a\in C_{\mathrm{odd}}(G)}\frac1a \geq\left(\frac12-o_k(1)\right)\log k.

The harmonic bound and infinite-chromatic implication include the reciprocal-sum estimate, its asymptotic sharpness, and the use of de Bruijn–Erdős compactness. This distinguishes the quantitative finite result from the passage to the infinite graph in the stated problem.

The site's historical remarks report that [Er81] asks about positive upper density, while [Er95d] and [Er96] ask about upper density or upper logarithmic density at least $1/2$ . It also notes that lower density may be zero, using graphs of arbitrarily high chromatic number and girth. These are recorded as the site's historical remarks; they are not additional formal-proof claims. See also Problem 65.

Known results and methods

Odd interval theorem: the full proof uses a minimal odd cycle of bipartite subgraphs, proves nonconsecutive members disjoint, and varies paths in a weighted independent collection.
Prescribed-length path theorem: supplies the common expander construction underlying both this problem and Problem 63. Its internal lemmas are stored once in the same source folder.
Finite-colour compactness: every graph of infinite chromatic number has finite subgraphs of arbitrarily high chromatic number.

Existing formalizations

The Lean development behind the site's qualifier is Erdos57.lean in Boris Alexeev's lean-proofs collection, added on 2026-08-17. It declares itself a formalization of a solution to the problem, names Erdős, Hajnal, Liu and Montgomery as its informal authors and Codex and GPT-5.6 Sol as its formal authors, and ends with the theorem erdos_57, that a graph whose chromatic number is $\top$ has a non-summable series of odd-cycle reciprocals, followed by #print axioms. It is linked from the claim page as a formalization; this corpus has not built it, so it gives no formalized evidence. The formal-conjectures catalog has carried 57.lean since 2026-09-09, a statement of the problem with its proof left as sorry, and since 2026-09-18 its formal_proof attribute points at that file at the commit linked above. The community database labeled the result Lean without a proof URL or a formalized statement at its revision of 2026-09-05 and records a formalized statement since 2026-09-09.

Other public Lean, at the pinned commit: a LeanGenius source file formalizes the statement but declares erdos_57 as an axiom, so its corollary about infinitely many odd lengths depends on that axiom and it is not a formal proof of the solving theorem. The same repository contains odd closed-walk lemmas and odd-girth lemmas, and its auxiliary Aristotle file and companion file contain sorry placeholders. The existing Mathlib formalization of Rado's selection principle covers a compactness dependency only.

Detailed references

[ErHa66] Erdős, P. and Hajnal, A., On chromatic number of graphs and set-systems, Acta Math. Acad. Sci. Hungar. 17 (1966), 61–99.
[Er81] Erdős, P., On the combinatorial problems which I would most like to see solved, Combinatorica (1981), 25–42.
[Er95d] Erdős, P., On some problems in combinatorial set theory, Publ. Inst. Math. (Beograd) (N.S.) 57(71) (1995), 61–65.
[Er96] Erdős, P., Some of my favourite problems on cycles and colourings, Tatra Mt. Math. Publ. (1996), 7–9.
[LiMo20] Liu, H. and Montgomery, R., A solution to Erdős and Hajnal's odd cycle problem, arXiv:2010.15802 (2020), v2 (2022); J. Amer. Math. Soc. 36 (2023), 1191–1234.
[dBEr51] de Bruijn, N. G. and Erdős, P., A colour problem for infinite graphs and a problem in the theory of relations, Indag. Math. 13 (1951), 371–373.

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.

Linked from (52)

Divergent odd-cycle reciprocals from the odd interval theorem problems/graph_coloring/E0057/claims Graph Coloring extremal_graph_theory/erdos_1975_recent_progress_extremal_problems_graph_theory Graph Coloring A slow edge-deletion budget forces three-colorability graph_coloring/bruijn_1951_colour_problem_infinite_graphs_problem_theory Compactness of finite graph colourings Rado selection principle graph_coloring/erdos_1995_problems_combinatorial_set_theory Section 9 (p. 65): the Erdős–Hajnal conjecture on reciprocal odd cycle lengths, and cycle lengths along a sequence of density 0 graph_coloring/liu_2020_solution_erdos_hajnal_s_odd_cycle One-step expansion under limited contact A first slow-growth ball has small neighbourhood Claim 4.4 (many separated simple adjusters)Claim 4.5 (many adjusters avoid high-degree vertices)Claim 4.6 (many adjusters avoid the large small-diameter set)Bipartite expander extraction Corollary 3.15 (two disjoint paths of prescribed total length)Long intervals of paths between every pair Sublinear expansion and path parity Limited contact Vertex expansion Definition 4.1 (adjusters)Disjoint small vertex expansions around prescribed roots Lemma 3.12 (a large bounded-diameter expansion)Lemma 3.13 (enlarging four rooted expansions)Lemma 3.14 (a long path between rooted expansions)Expansion while avoiding three sets Short path between two sets after a small deletion Few disjoint slowly expanding low-contact sets One of many separated sets expands Lemma 4.2 (one simple adjuster)Lemma 4.3 (robust simple adjusters)Lemma 4.7 (chaining simple adjusters)Lemma 4.8 (a path of a prescribed length between expansions)Odd cycle harmonic sum and the infinite-chromatic consequence Shrinking a vertex expansion Proposition 3.16 (a subdivided clique in a skewed bipartite pair)A bound for successive fractional powers Parity identities in a bipartite graph Intervals of odd cycle lengths from chromatic number Theorem 2.7 (prescribed path lengths in bipartite expanders)integer_sequences/erdos_1997_some_old_new_problems_various_branches_combinatorics ramsey_theory/erdos_1996_some_my_favourite_problems_cycles_colourings set_systems/erdos_1981_combinatorial_problems_which_i_would_most Rado (1949): Axiomatic treatment of rank in infinite sets Lemma 1: Rado's finite-choice selection principle set_theory/erdos_1966_chromatic_number_graphs_set_systems Problem 7.8: reciprocal sum of circuit lengths at chromatic number ω

Graph