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

Updated Oct 8

Problem 63

claims/: The 2 claim pages of Problem 63, one per claimant's result; the problem's standing derives from them.

Statement. Does every graph with infinite chromatic number contain a cycle of length $2^n$ for infinitely many $n$ ?

Status. The site labels the problem PROVED (LEAN) and credits Zach Hunter with deducing it from Liu and Montgomery's even-cycle interval theorem; the Lean behind the qualifier is described below. The accepted full claim is powers of two from the even-cycle interval theorem; the uncountable-chromatic case is an accepted partial claim, every power of two at uncountable chromatic number.

Source. T. F. Bloom, Erdős Problem #63, erdosproblems.com/63, accessed 2026-09-05. On that date the discussion thread held one comment, of 15 November 2025, reporting a broken [dBEr51] reference and marked addressed by the site, and the proof-claims thread was empty.

References. Original problem references, as listed by the site: [Er93, p. 342], [Er94b], [Er95], [Er95d], [Er96], [Er97b]. Of these, [Er97b] (Erdős, Some old and new problems in various branches of combinatorics, Discrete Math. 165/166 (1997), 227--231) states the Erdős--Mihók conjecture as item 3 on p. 228, quoted on its card, erdos_1997_some_old_new_problems_various_branches_combinatorics.

Formalization. A public Lean 4 proof, cited by the formal-conjectures catalog as the problem's formal proof, is linked from the claim page; see Existing formalizations below.

Current assessment

Claims. The full claim page is accepted on the curator's credit alone: the theorem it rests on is refereed (J. Amer. Math. Soc. 36 (2023)), but the problem's statement is a deduction recorded on the site, not a theorem of the paper, so the page lists no refereed evidence; the public Lean proof of the statement, which declares itself a formalization of Liu and Montgomery's solution, is a formalization link on the page and not formalized evidence, because this corpus has not built it. The uncountable-chromatic case, which the site credits to David Penman's observation from a theorem of Erdős and Hajnal [ErHa66], is an accepted partial claim (claim page), filed under that theorem as the full claim is filed under Liu and Montgomery's. It is refereed because the cycles are subgraphs of what the theorem supplies.

Compilation coverage. The library's compilation of the Liu–Montgomery proof chain is incomplete at Lemma 3.13’s reservoir compatibility step; the compactness and uncountable-chromatic arguments are compiled in full. Compilation coverage is separate from the problem's standing.

Progress

The site attributes the conjecture to Mihók and Erdős. It records Zach Hunter's observation that the answer follows from Liu–Montgomery, Theorem 1.1: a finite graph of sufficiently large average degree $d$ contains every even cycle length in

[(\log L)^8,L],\qquad L\geq\frac{d}{10\log^{12}d}.

De Bruijn–Erdős compactness supplies finite subgraphs of unbounded chromatic number, and their critical subgraphs have unbounded minimum degree. Thus $L$ becomes unbounded. The complete implication for Problem 63 chooses the largest power of two at most $L$ and checks that it belongs to the even-cycle interval. Its exponent tends to infinity, proving the required infinitude of distinct powers.

The same interval theorem yields unavoidability for much more general even sequences. This is a shared method, not an independent proof. The site also mentions possible replacements of powers of two by other sequences, including squares, and links Problem 64. The theorem at high average degree does not by itself settle the specific minimum-degree-three assertion of #64.

The uncountable-chromatic case

The site credits David Penman with a separate observation: if $\chi(G)>\aleph_0$ , an Erdős–Hajnal theorem supplies arbitrarily large finite complete bipartite subgraphs. In the stronger formulation of Reiher, Theorem 3.17, $G$ contains $K_{n,\aleph_1}$ for every positive integer $n$ . This includes a cycle of length $2^m$ for every $m\geq2$ , by taking $n=2^{m-1}$ and alternating the $n$ vertices in its finite side with $n$ distinct vertices in the other side. The original source is Erdős–Hajnal, Corollary 5.6.

This route uses cardinal coloring and bipartite containment; it is materially different from the quantitative finite-expander method. Its uncountable-chromatic hypothesis is stronger than the problem's hypothesis, so it does not cover graphs of chromatic number $\aleph_0$ . This case is the accepted partial claim of the problem.

Existing formalizations

The community database (teorth/erdosproblems), at 2026-10-07, lists the problem as proved (Lean) as of its last update on 2026-08-24 and as formalized as of that field's last update on 2026-09-09, with no proof URL of its own. The formal-conjectures catalog's statement file 63.lean, added 2026-09-09, states the problem as erdos_63 with answer(True), is tagged research solved and, since 2026-09-18, cites as its formal proof the Lean 4 file Erdos63.lean in Boris Alexeev's lean-proofs repository, added 2026-08-17. That file declares itself a formalization of a solution to the problem, names Hong Liu and Richard Montgomery as its informal authors and Codex and GPT-5.6 Sol as its formal authors, and its theorem erdos_63 states that a simple graph whose chromatic number is $\top$ has a cycle of length $2^n$ for infinitely many $n$ . The claim page links the file at the commit the catalog cites; this corpus has not built it, so it is a link and not formalized evidence.

An earlier LeanGenius source file formalizes the statement but declares erdos_63_theorem as an axiom; its infinitude corollary invokes that axiom, so it is a statement with conditional consequences, not a formal proof of the problem. The Mathlib formalization of Rado's selection principle is a dependency-level formalization.

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.
[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.
[Re24] Reiher, C., Graphs of large girth, arXiv:2403.13571 (2024).
[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)

Problem 57 Every power of two at uncountable chromatic number Powers of two from the even-cycle interval theorem problems/graph_coloring/E0063/claims Graph Coloring 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)Unavoidable even sequences Bipartite expander extraction Corollary 3.15 (two disjoint paths of prescribed total length)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)Unbounded powers of two as cycle lengths Shrinking a vertex expansion Proposition 3.16 (a subdivided clique in a skewed bipartite pair)A bound for successive fractional powers Intervals of even cycle lengths from average degree Theorem 2.7 (prescribed path lengths in bipartite expanders)graph_coloring/reiher_2024_graphs_large_girth Theorem 3.17: complete bipartite subgraphs at uncountable chromatic number integer_sequences/erdos_1997_some_old_new_problems_various_branches_combinatorics 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 Corollary 5.6: complete bipartite subgraphs from uncountable colouring number

Graph