Erdős Problem 600 to Erdős Problem 628

TheoremErdős Problem 600#

Reference: - erdosproblems.com/600 - erdosproblems.com/80 - [Er87] Erdős, P., Some problems on finite and infinite graphs. Logic and combinatorics (Arcata, Calif., 1985) (1987), 223-228. - [RuSz78] Ruzsa, I. Z. and Szemerédi, E., Triple systems with no six points carrying three triangles. Combinatorics (Proc. Fifth Hungarian Colloq., Keszthely, 1976), Vol. II (1978), 939-945.

Quoted from FormalConjectures/ErdosProblems/600.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/600.

The file states 3 research or textbook statements: 2 open and 1 solved.

Erdos600.erdos_600.parts.i

Open: stated without proof.

Let \(r \geq 2\). Is it true that \(e(n,r+1) - e(n,r) \to \infty\) as \(n \to \infty\)?

theorem erdos_600.parts.i :
    ∀ r : ℕ, 2 ≤ r →
      Tendsto (fun (n : ℕ) ↦ (eFunction n (r + 1) : ℝ) - (eFunction n r : ℝ)) atTop atTop

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/600.lean, line 53.

Erdos600.erdos_600.parts.ii

Open: stated without proof.

Let \(r \geq 2\). Is it true that \(\frac{e(n,r+1)}{e(n,r)} \to 1\) as \(n \to \infty\)?

theorem erdos_600.parts.ii :
    ∀ r : ℕ, 2 ≤ r →
      Tendsto (fun (n : ℕ) ↦ (eFunction n (r + 1) : ℝ) / (eFunction n r : ℝ)) atTop (𝓝 1)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/600.lean, line 62.

Erdos600.erdos_600.variants.ruzsa_szemeredi_upper_bound

Solved: stated here without proof.

Ruzsa and Szemerédi [RuSz78] proved that \(e(n,r)=o(n^2)\) for any fixed \(r\).

theorem erdos_600.variants.ruzsa_szemeredi_upper_bound :
    ∀ r : ℕ, (fun (n : ℕ) ↦ (eFunction n r : ℝ)) =o[atTop] (fun (n : ℕ) ↦ (n : ℝ)^2)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/600.lean, line 71.

Sources

• FormalConjectures/ErdosProblems/600.lean at 2055e5ad
• erdosproblems.com/600

LeanErdos600.erdos_600.parts.i · Erdos600.erdos_600.parts.ii · Erdos600.erdos_600.variants.ruzsa_szemeredi_upper_bound

TheoremErdős Problem 601#

Reference: erdosproblems.com/601

References: - [EHM70] Erdős, P.; Hajnal, A.; Milner, E.C. Set mappings and polarized partition relations. Combinatorial theory and its applications, I–III (Balatonfüred, 1969) (1970), 327–363. - [Er81] Erdős, P. On the combinatorial problems which I would most like to see solved. Combinatorica 1 (1981), 25–42, Section VII. - [La90] Larson, J.A. Martin's Axiom and ordinal graphs: large independent sets or infinite paths. Ann. Pure Appl. Logic 47 (1990), 31–39.

Quoted from FormalConjectures/ErdosProblems/601.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/601.

The file states 5 research or textbook statements: 3 open and 2 solved.

Erdos601.erdos_601

Open: stated without proof.

Erdős Problem 601 ($500 prize).

For which limit ordinals \(\alpha\) does HasPathOrIndepSetOfType α hold?

theorem erdos_601 :
    ∀ α : Ordinal.{0}, Order.IsSuccLimit α →
      (HasPathOrIndepSetOfType α ↔
        erdos_601.answer α)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/601.lean, line 66.

Erdos601.erdos_601.variants.universal

Open: stated without proof.

Erdős–Hajnal–Milner conjecture [Er81, Section VII]: every graph on a limit ordinal \(\alpha\) contains an infinite path or an independent set of order type \(\alpha\).

theorem erdos_601.variants.universal :
    ∀ α : Ordinal.{0}, Order.IsSuccLimit α → HasPathOrIndepSetOfType α

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/601.lean, line 76.

Erdos601.erdos_601.variants.erdos_hajnal_milner_1970

Solved: stated here without proof.

Erdős–Hajnal–Milner (1970) [EHM70]: For all limit ordinals \(\alpha < \omega_1^{\omega+2}\), every graph on \(\alpha.\mathrm{ToType}\) has either an infinite path or an independent set of order type \(\alpha\).

theorem erdos_hajnal_milner_1970 :
    ∀ α : Ordinal.{0},
      Order.IsSuccLimit α →
      α < ω_ 1 ^ (ω + 2) →
      HasPathOrIndepSetOfType α

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/601.lean, line 88.

Erdos601.erdos_601.variants.omega_1_omega_plus_2

Open: stated without proof.

Erdős–Hajnal–Milner conjecture at \(\omega_1^{\omega+2}\) [Er81, Section VII]: every graph on \(\omega_1^{\omega+2}\) contains an infinite path or an independent set of that order type. Erdős conjectured the positive answer. This is the first limit ordinal not covered by the Erdős–Hajnal–Milner theorem.

theorem omega_1_omega_plus_2 :
    HasPathOrIndepSetOfType (ω_ 1 ^ (ω + 2))

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/601.lean, line 102.

Erdos601.erdos_601.variants.at_omega

Solved: stated here without proof.

Base case \(\alpha = \omega\): HasPathOrIndepSetOfType ω holds.

Every countably infinite graph on vertex set \(\omega\) either contains an infinite path or has an infinite independent set (and an infinite set has order type \(\omega\)). Follows from Ramsey-theoretic arguments (or directly from the Erdős–Hajnal–Milner result since \(\omega < \omega_1^{\omega+2}\)).

theorem at_omega : HasPathOrIndepSetOfType ω

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/601.lean, line 122.

Sources

• FormalConjectures/ErdosProblems/601.lean at 2055e5ad
• erdosproblems.com/601

LeanErdos601.erdos_601 · Erdos601.erdos_601.variants.universal · Erdos601.erdos_601.variants.erdos_hajnal_milner_1970 · Erdos601.erdos_601.variants.omega_1_omega_plus_2 · Erdos601.erdos_601.variants.at_omega

TheoremErdős Problem 602#

Reference: erdosproblems.com/602

Quoted from FormalConjectures/ErdosProblems/602.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/602.

The file states 8 research or textbook statements: 1 open, 4 solved and 3 textbook results.

Erdos602.erdos_602

Open: stated without proof.

Does every almost-disjoint family of countably infinite sets whose pairwise intersections all have size ≠ 1 have Property B?

Formally: let α be any type, let (A_i)_{i ∈ I} be a family of countably infinite subsets of α such that for all i ≠ j, the intersection A_i ∩ A_j is finite and |A_i ∩ A_j| ≠ 1. Does there exist a 2-colouring f : α → Fin 2 such that no A_i is monochromatic?

This is an open question about Property B for almost-disjoint families with a forbidden intersection size of 1.

Note: This generalises the formulation in which the ground set is ℕ. Since every countably infinite set is in bijection with ℕ, the two formulations are equivalent, but working over an arbitrary ground type makes the statement apply immediately to, e.g., almost-disjoint families of countable subsets of an uncountable space.

theorem erdos_602 :
    ∀ {α : Type*} {I : Type*} (A : I → Set α),
      (∀ i, (A i).Countable ∧ (A i).Infinite) →
      (∀ i j, i ≠ j → (A i ∩ A j).Finite) →
      (∀ i j, i ≠ j → Set.ncard (A i ∩ A j) ≠ 1) →
      HasPropertyB I A

Category research open; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/602.lean, line 78.

Erdos602.erdos_602.variants.disjoint

Proved here.

Trivial case: pairwise disjoint families.

If the A_i are pairwise disjoint (all intersections are empty, which in particular satisfies |A_i ∩ A_j| ≠ 1), then Property B holds trivially.

Proof sketch: Since each A_i is infinite, it has (at least) two distinct elements a_i and b_i. We can define a colouring that assigns colour 0 to a_i and colour 1 to b_i for each i (using disjointness, these choices don't conflict), and extend arbitrarily elsewhere. Then no A_i is monochromatic.

theorem erdos_602.variants.disjoint :
    ∀ {α : Type*} {I : Type*} (A : I → Set α),
      (∀ i, (A i).Infinite) →
      (∀ i j, i ≠ j → Disjoint (A i) (A j)) →
      HasPropertyB I A

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/602.lean, line 99.

Erdos602.erdos_602.variants.countable_index

Solved: stated here without proof.

Countable index set case.

If the index set is countable, the answer is yes, and the intersection condition is unnecessary. This is Bernstein's Lemma: every countable system of infinite sets has Property B.

theorem erdos_602.variants.countable_index :
    ∀ {α : Type*} (A : ℕ → Set α),
      (∀ i, (A i).Countable ∧ (A i).Infinite) →
      (∀ i j, i ≠ j → (A i ∩ A j).Finite) →
      (∀ i j, i ≠ j → Set.ncard (A i ∩ A j) ≠ 1) →
      HasPropertyB ℕ A

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/602.lean, line 156.

Erdos602.erdos_602.variants.single_set

Textbook result, proved here.

Intersections of size ≥ 2 suffice.

For a single countably infinite set A ⊆ α, there trivially exists a 2-colouring of α that makes A non-monochromatic: since A is infinite, it has two distinct elements, so any colouring that assigns them different colours works.

theorem erdos_602.variants.single_set {α : Type*} (A : Set α) (hA : A.Infinite) :
    ∃ f : α → Fin 2, ¬IsMonochromatic f A

Category textbook; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/602.lean, line 171.

Erdos602.erdos_602.variants.empty_index

Textbook result, proved here.

Empty index set.

If the index set I is empty (has no elements), then Property B holds vacuously: any 2-colouring works, since there are no sets to be made non-monochromatic.

theorem erdos_602.variants.empty_index {α : Type*} :
    ∀ (A : PEmpty → Set α),
      (∀ i, (A i).Infinite) →
      HasPropertyB PEmpty A

Category textbook; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/602.lean, line 204.

Erdos602.erdos_602.variants.unique_index

Textbook result, proved here.

Unique index set.

If the index set has exactly one element (i.e., [Unique I]), then Property B holds: any 2-colouring that makes the single set A (default : I) non-monochromatic works. This follows from the single-set case.

theorem erdos_602.variants.unique_index {α : Type*} (I : Type*) [Unique I]
    (A : I → Set α) (hInfinite : ∀ i, (A i).Infinite) :
    HasPropertyB I A

Category textbook; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/602.lean, line 218.

Erdos602.erdos_602.variants.two_sets

Proved here.

Two infinite sets with pairwise intersection of size ≠ 1.

If the family consists of exactly two countably infinite sets A₀ and A₁ with |A₀ ∩ A₁| ≠ 1 (and finite), then Property B holds.

Proof sketch: - If A₀ ∩ A₁ = ∅: the sets are disjoint. Pick distinct a, b ∈ A₀ and distinct c, d ∈ A₁. Colour b and c with 1, everything else with 0. Then A₀ has a (colour 0) and b (colour 1), and A₁ has c (colour 1) and d (colour 0), so neither is monochromatic. - If |A₀ ∩ A₁| ≥ 2: the intersection contains two distinct points x and y. Assign x colour 0 and y colour 1. Both A₀ and A₁ contain x and y, so neither is monochromatic.

theorem erdos_602.variants.two_sets :
    ∀ {α : Type*} (A : Fin 2 → Set α),
      (∀ i, (A i).Infinite) →
      (A 0 ∩ A 1).Finite →
      Set.ncard (A 0 ∩ A 1) ≠ 1 →
      HasPropertyB (Fin 2) A

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/602.lean, line 243.

Erdos602.disjoint_without_infinite_claim.disproof

Proved here.

Formal disproof of disjoint_without_infinite_claim.

Counterexample: Take α = ℕ, I = Fin 2, with A 0 = {0} and A 1 = {1}. These are pairwise disjoint, satisfying the only hypothesis. But singleton sets are vacuously monochromatic under any colouring: the only pair (x, y) ∈ {0} × {0} is (0, 0), and f 0 = f 0 trivially. So any colouring makes A 0 monochromatic, meaning HasPropertyB fails.

theorem disjoint_without_infinite_claim.disproof :
    ¬ disjoint_without_infinite_claim

Category research solved; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/602.lean, line 449.

Sources

• FormalConjectures/ErdosProblems/602.lean at 2055e5ad
• erdosproblems.com/602

LeanErdos602.erdos_602 · Erdos602.erdos_602.variants.disjoint · Erdos602.erdos_602.variants.countable_index · Erdos602.erdos_602.variants.single_set · Erdos602.erdos_602.variants.empty_index · Erdos602.erdos_602.variants.unique_index · Erdos602.erdos_602.variants.two_sets · Erdos602.disjoint_without_infinite_claim.disproof

TheoremErdős Problem 603#

References: - erdosproblems.com/603

Quoted from FormalConjectures/ErdosProblems/603.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/603.

The file states 1 research or textbook statement: 1 solved.

Erdos603.erdos_603

Solved: stated here without proof.

Let \((A_i)\) be a family of countably infinite sets such that \(\lvert A_i\cap A_j\rvert \neq 2\) for all \(i\neq j\). Find the smallest cardinal \(C\) such that \(\cup A_i\) can always be coloured with at most \(C\) colours so that no \(A_i\) is monochromatic.

GPT 5.4 Pro (prompted by Chojecki) proved there is no uniform bound on such \(C\): for every cardinal \(C\) there is a family of countably infinite sets \((A_i)\) such that \(\lvert A_i\cap A_j\rvert \neq 2\) for all \(i\neq j\), and in any colouring of \(\cup A_i\) with \(C\) colours some \(A_i\) is monochromatic.

theorem erdos_603 :
    ∀ C : Cardinal.{0}, ∃ (V : Type) (F : Set (Set V)),
    (∀ A ∈ F, Cardinal.mk A = ℵ₀) ∧
    F.Pairwise (fun (A B : Set V) ↦ Cardinal.mk ↥(A ∩ B) ≠ 2) ∧
    ⋃₀ F = Set.univ ∧
    ∀ c : V → C.out, ∃ A ∈ F, ∀ x ∈ A, ∀ y ∈ A, c x = c y

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/603.lean, line 43.

Sources

• FormalConjectures/ErdosProblems/603.lean at 2055e5ad
• erdosproblems.com/603

LeanErdos603.erdos_603

TheoremErdős Problem 604#

References: - erdosproblems.com/604 - [OAI26] OpenAI, The weak pinned planar distance theorem (2026). - [Er46] Erdős, Paul, On sets of distances of \(n\) points. Amer. Math. Monthly (1946), 248--250. - [Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108. - [Er83c] Erdős, Paul, Combinatorial problems in geometry. Math. Chronicle (1983), 35-54. - [Er85] Erdős, P., Problems and results in combinatorial geometry. Discrete geometry and convexity (New York, 1982) (1985), 1-11. - [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177. - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10. - [KaTa04] Katz, Nets Hawk and Tardos, Gábor, A new entropy inequality for the Erdős distance problem. Towards a theory of geometric graphs (2004), 119-126.

Quoted from FormalConjectures/ErdosProblems/604.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/604.

The file states 5 research or textbook statements: 2 open and 3 solved.

Erdos604.erdos_604

Solved: stated here; a Lean proof is at https://github.com/MendozaLab/erdos-experiments/blob/09f72c57ed2d98906b9cf03bff2091f6fe73807f/proofs/erdos604/Erdos604Proof/ExternalApplication.lean#L17.

Given \(n\) distinct points \(A\subset\mathbb{R}^2\), must there be a point \(x\in A\) such that

\[\#\{ d(x,y) : y \in A\} \gg n^{1-o(1)}?\]

This is the pinned distance problem, a stronger form of Problem 89. Here \(n^{1-o(1)}\) means: for every \(\varepsilon > 0\) and all large \(n\), the bound is at least \(n^{1-\varepsilon}\). We do not count the distance \(d(x, x) = 0\); this changes the count by one.

This weak formulation was proved by OpenAI [OAI26].

theorem erdos_604 :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop,
      (n : ℝ) ^ (1 - ε) ≤ (pinnedDistinctDistances n : ℝ)

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/604.lean, line 82.

Erdos604.erdos_604.variants.sqrt_log

Open: stated without proof.

Given \(n\) distinct points \(A\subset\mathbb{R}^2\), must there be a point \(x\in A\) such that

\[\#\{ d(x,y) : y \in A\} \gg \frac{n}{\sqrt{\log n}}?\]

theorem erdos_604.variants.sqrt_log :
    (fun n : ℕ => (n : ℝ) / (n : ℝ).log.sqrt) =O[atTop]
      (fun n => (pinnedDistinctDistances n : ℝ))

Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/604.lean, line 92.

Erdos604.erdos_604.variants.grid_upper_bound

Solved: stated here without proof.

The integer grid shows that \(\frac{n}{\sqrt{\log n}}\) would be best possible: there are sets of \(n\) points in \(\mathbb{R}^2\) in which every point has \(O(\frac{n}{\sqrt{\log n}})\) distinct distances to the other points. This follows from the bound of Erdős [Er46] on the total number of distinct distances in the grid (see Erdős Problem 89), since the number of distances from one point is at most the total number of distances. For \(n\) that is not a square, take \(n\) points of the smallest square grid with at least \(n\) points.

theorem erdos_604.variants.grid_upper_bound :
    (fun n => (pinnedDistinctDistances n : ℝ)) =O[atTop]
      (fun n : ℕ => (n : ℝ) / (n : ℝ).log.sqrt)

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/604.lean, line 106.

Erdos604.erdos_604.variants.katz_tardos

Solved: stated here without proof.

Katz and Tardos [KaTa04] proved that some point of \(A\) has \(\gg n^{c-o(1)}\) distinct distances to the other points of \(A\), where

\[c=\frac{48-14e}{55-16e}=0.864137\cdots.\]

theorem erdos_604.variants.katz_tardos :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop,
      (n : ℝ) ^ ((48 - 14 * Real.exp 1) / (55 - 16 * Real.exp 1) - ε) ≤
        (pinnedDistinctDistances n : ℝ)

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/604.lean, line 117.

Erdos604.erdos_604.variants.average

Open: stated without proof.

Let \(d(x)\) be the number of distinct distances from \(x\) to the other points of \(A\). Erdős [Er75f] conjectured that

\[\sum_{x\in A}d(x) \gg \frac{n^2}{\sqrt{\log n}}\]

for every set \(A\subset\mathbb{R}^2\) of \(n\) points.

The sum is at most \(n\) times the largest \(d(x)\), so this conjecture implies a positive answer to Erdos604.erdos_604.variants.sqrt_log.

theorem erdos_604.variants.average :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℝ², #A = n →
      C * (n : ℝ) ^ 2 / (n : ℝ).log.sqrt ≤ ((∑ x ∈ A, distinctDistancesFrom A x : ℕ) : ℝ)

Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/604.lean, line 133.

Sources

• FormalConjectures/ErdosProblems/604.lean at 2055e5ad
• erdosproblems.com/604

LeanErdos604.erdos_604 · Erdos604.erdos_604.variants.sqrt_log · Erdos604.erdos_604.variants.grid_upper_bound · Erdos604.erdos_604.variants.katz_tardos · Erdos604.erdos_604.variants.average

TheoremErdős Problem 609#

References: - erdosproblems.com/609 - [ErGr75] Erdős, P. and Graham, R. L., On partition theorems for finite graphs. Colloq. Math. Soc. János Bolyai (1975). - [Ch97] Chung, F., Open problems of Paul Erdős in graph theory. J. Graph Theory (1997), 3-36. - [DaJo17] Day, A. N. and Johnson, J. R., Multicolour Ramsey numbers of odd cycles. J. Combin. Theory Ser. B (2017), 56-63. - [GiHu24] Girão, A. and Hunter, Z., Monochromatic odd cycles in edge-coloured complete graphs. arXiv:2412.07708 (2024). - [JaYi25] Janzer, O. and Yip, F., Short monochromatic odd cycles. arXiv:2506.14910 (2025).

Quoted from FormalConjectures/ErdosProblems/609.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/609.

The file states 1 research or textbook statement: 1 open.

Erdos609.erdos_609

Open: stated without proof.

Let \(f(n)\) be the minimal \(m\) such that if the edges of \(K_{2^n+1}\) are coloured with \(n\) colours then there must be a monochromatic odd cycle of length at most \(m\). Estimate \(f(n)\).

theorem erdos_609 :
    (fun n ↦ (f n : ℝ)) =Θ[atTop] erdos_609.answer

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/609.lean, line 68.

Sources

• FormalConjectures/ErdosProblems/609.lean at 2055e5ad
• erdosproblems.com/609

LeanErdos609.erdos_609

TheoremErdős Problem 611#

References: - erdosproblems.com/611 - [EGT92] Erdős, Paul and Gallai, Tibor and Tuza, Zsolt, Covering the cliques of a graph with vertices. Discrete Math. (1992), 279-289. - [Er94] Erdős, P., Problems and results on set systems and hypergraphs. Extremal problems for finite sets (Visegrád, 1991) (1994), 217-227. - [Er99] Erdős, Paul, A selection of problems and results in combinatorics. Combin. Probab. Comput. (1999), 1-6.

Quoted from FormalConjectures/ErdosProblems/611.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/611.

The file states 4 research or textbook statements: 2 open and 2 solved.

Erdos611.erdos_611.parts.i

Open: stated without proof.

For a graph \(G\) let \(\tau(G)\) denote the minimal number of vertices that include at least one from each maximal clique of \(G\). Is it true that if all maximal cliques in \(G\) have at least \(cn\) vertices then \(\tau(G) = o_c(n)\)?

Here \(n\) is the number of vertices, and \(o_c(n)\) is uniform over all such graphs on \(n\) vertices. \(\tau(G)\) is SimpleGraph.cliqueTransversalNumber, which (as in Erdős Problem 151) ignores maximal cliques on one vertex; this makes no difference here, since for large \(n\) every maximal clique has at least \(cn \geq 2\) vertices.

theorem erdos_611.parts.i :
    ∀ c > (0 : ℝ), ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
      AllMaximalCliquesAtLeast G (c * (n : ℝ)) →
        (G.cliqueTransversalNumber : ℝ) ≤ ε * (n : ℝ)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/611.lean, line 66.

Erdos611.erdos_611.parts.ii

Open: stated without proof.

For \(0 < c < 1\), estimate the minimal \(k_c(n)\) such that if every maximal clique in a graph \(G\) on \(n\) vertices has at least \(k_c(n)\) vertices then \(\tau(G) < (1 - c)n\).

We require \(c < 1\): for \(c \geq 1\) the bound \(\tau(G) < (1 - c)n \leq 0\) is impossible, so \(k_c(n)\) is degenerate. Erdős, Gallai, and Tuza [EGT92] proved a lower bound of the form \(k_c(n) \geq n^{c'/\log\log n}\) for some \(c' > 0\) (as reported on erdosproblems.com).

theorem erdos_611.parts.ii :
    ∀ c : ℝ, 0 < c → c < 1 →
      (fun n ↦ (cliqueThreshold c n : ℝ)) =Θ[atTop] erdos_611.parts.ii.answer c

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/611.lean, line 83.

Erdos611.erdos_611.variants.bollobas_erdos

Solved: stated here without proof.

Bollobás and Erdős proved that if every maximal clique of a graph \(G\) on \(n\) vertices has at least \(n + 3 - 2\sqrt{n}\) vertices then \(\tau(G) = 1\) (as reported on erdosproblems.com).

theorem erdos_611.variants.bollobas_erdos :
    ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
      AllMaximalCliquesAtLeast G ((n : ℝ) + 3 - 2 * Real.sqrt (n : ℝ)) →
        G.cliqueTransversalNumber = 1

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/611.lean, line 93.

Erdos611.erdos_611.variants.bollobas_erdos_sharp

Solved: stated here without proof.

The threshold \(n + 3 - 2\sqrt{n}\) of Bollobás and Erdős is best possible. We formalise this as: for every \(n = m^2\) with \(m \geq 2\) there is a graph on \(n\) vertices whose maximal cliques all have at least \(n + 2 - 2\sqrt{n} = m^2 + 2 - 2m\) vertices and with \(\tau(G) \geq 2\).

theorem erdos_611.variants.bollobas_erdos_sharp :
    ∀ m : ℕ, 2 ≤ m → ∃ G : SimpleGraph (Fin (m ^ 2)),
      AllMaximalCliquesAtLeast G ((m : ℝ) ^ 2 + 2 - 2 * (m : ℝ)) ∧
        2 ≤ G.cliqueTransversalNumber

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/611.lean, line 105.

Sources

• FormalConjectures/ErdosProblems/611.lean at 2055e5ad
• erdosproblems.com/611

LeanErdos611.erdos_611.parts.i · Erdos611.erdos_611.parts.ii · Erdos611.erdos_611.variants.bollobas_erdos · Erdos611.erdos_611.variants.bollobas_erdos_sharp

TheoremErdős Problem 613#

Reference: erdosproblems.com/613

Quoted from FormalConjectures/ErdosProblems/613.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/613.

The file states 1 research or textbook statement: 1 solved.

Erdos613.erdos_613

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos613.lean#L1170.

Erdős Problem 613: Let \(n \geq 3\) and \(G\) be a graph with \(\binom{2n+1}{2} - \binom{n}{2} - 1\) edges. Must \(G\) be the union of a bipartite graph and a graph with maximum degree less than \(n\)?

theorem erdos_613 :
    ¬ ∀ n ≥ 3, ∀ (V : Type*) [Fintype V] (G : SimpleGraph V), [DecidableRel G.Adj] →
      G.edgeFinset.card = Nat.choose (2 * n + 1) 2 - Nat.choose n 2 - 1 →
      ∃ (B D : SimpleGraph V), [DecidableRel B.Adj] → [DecidableRel D.Adj] →
        G = B ⊔ D ∧ B.IsBipartite ∧ ∀ v, D.degree v < n

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/613.lean, line 37.

Sources

• FormalConjectures/ErdosProblems/613.lean at 2055e5ad
• erdosproblems.com/613

LeanErdos613.erdos_613

TheoremErdős Problem 614#

References: - erdosproblems.com/614 - A problem on sparse induced subgraphs - [FRS97] Faudree, R. J., Rousseau, C. C. and Schelp, R. H., Problems in graph theory from Memphis. The Mathematics of Paul Erdős, II, 7–26.

Quoted from FormalConjectures/ErdosProblems/614.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/614.

The file states 1 research or textbook statement: 1 open.

Erdos614.erdos_614

Open: stated without proof.

Let \(f(n,k)\) be minimal such that there is a graph with \(n\) vertices and \(f(n,k)\) edges where every set of \(k+2\) vertices induces a subgraph with maximum degree at least \(k\). Determine \(f(n,k)\).

theorem erdos_614 :
    ∀ n k, IsLeast {m : ℕ | ∃ G : SimpleGraph (Fin n), G.edgeFinset.card = m ∧
      ∀ s : Finset (Fin n), s.card = k + 2 →
        ∃ v : s, k ≤ (G.induce (s : Set (Fin n))).degree v} (erdos_614.answer n k)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/614.lean, line 43.

Sources

• FormalConjectures/ErdosProblems/614.lean at 2055e5ad
• erdosproblems.com/614

LeanErdos614.erdos_614

TheoremErdős Problem 615#

A Ramsey–Turán problem of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS93]: does there exist a constant \(c > 0\) such that every graph on \(n\) vertices with at least \((1/8 - c)n^2\) edges contains either a \(K_4\) or an independent set on at least \(n/\log n\) vertices? In the notation of Ramsey–Turán theory this asks whether

\[\mathrm{rt}(n; 4, n/\log n) < (1/8 - c)n^2.\]

This was disproved by Fox, Loh, and Zhao [FLZ15], who showed that \(\mathrm{rt}(n; 4, ne^{-f(n)}) \geq (1/8 - o(1))n^2\) whenever \(f(n) = o(\sqrt{\log n/\log\log n})\). In the other direction Sudakov [Su03] had shown that \(\mathrm{rt}(n; 4, ne^{-f(n)}) = o(n^2)\) whenever \(f(n)/\sqrt{\log n} \to \infty\).

References: * erdosproblems.com/615 * [EHSSS93] Erdős, P., Hajnal, A., Simonovits, M., Sós, V. T., and Szemerédi, E., Turán-Ramsey theorems and simple asymptotically extremal structures. Combinatorica 13 (1993), 31--56. * [Su03] Sudakov, B., A few remarks on Ramsey-Turán-type problems. J. Combin. Theory Ser. B 88 (2003), 99--106. * [FLZ15] Fox, J., Loh, P.-S., and Zhao, Y., The critical window for the classical Ramsey-Turán problem. Combinatorica 35 (2015), 435--476.

Quoted from FormalConjectures/ErdosProblems/615.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/615.

The file states 3 research or textbook statements: 3 solved. It also has 1 test statement, counted here but not shown.

Erdos615.erdos_615

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/dfe2d78128b493c572cf525b1b8edf4897fb7664/src/latest/ErdosProblems/Erdos615.lean#L492.

Does there exist some constant \(c > 0\) such that for all sufficiently large \(n\), if \(G\) is a graph with \(n\) vertices and at least \((1/8 - c)n^2\) edges then \(G\) must contain either a \(K_4\) or an independent set on at least \(n/\log n\) vertices?

The answer is no, as shown by Fox, Loh, and Zhao [FLZ15].

theorem erdos_615 :
    ¬ ∃ c : ℝ, 0 < c ∧ ∀ᶠ (n : ℕ) in atTop,
      ∀ G : SimpleGraph (Fin n), (1 / 8 - c) * n ^ 2 ≤ G.edgeFinset.card →
        ¬ G.CliqueFree 4 ∨ (n : ℝ) / Real.log n ≤ G.indepNum

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/615.lean, line 62.

Erdos615.erdos_615.variants.fox_loh_zhao

Solved: stated here without proof.

The result of Fox, Loh, and Zhao [FLZ15] disproving the problem: if \(f(n) \geq 0\) satisfies \(f(n) = o(\sqrt{\log n/\log\log n})\), then for every \(\epsilon > 0\) and all sufficiently large \(n\) there is a \(K_4\)-free graph on \(n\) vertices with independence number at most \(ne^{-f(n)}\) and at least \((1/8 - \epsilon)n^2\) edges; that is, \(\mathrm{rt}(n; 4, ne^{-f(n)}) \geq (1/8 - o(1))n^2\). Applied with \(f(n) = \log\log n\), this disproves the headline problem, since \(ne^{-f(n)} = n/\log n = o(n)\).

theorem erdos_615.variants.fox_loh_zhao (f : ℕ → ℝ) (hf : ∀ n, 0 ≤ f n)
    (hfo : Tendsto (fun n : ℕ => f n / Real.sqrt (Real.log n / Real.log (Real.log n)))
      atTop (nhds 0)) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ (n : ℕ) in atTop,
      ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
        (G.indepNum : ℝ) ≤ n * Real.exp (-f n) ∧
        (1 / 8 - ε) * n ^ 2 ≤ G.edgeFinset.card

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/615.lean, line 79.

Erdos615.erdos_615.variants.sudakov

Solved: stated here without proof.

The complementary result of Sudakov [Su03]: if \(f(n)/\sqrt{\log n} \to \infty\) then \(\mathrm{rt}(n; 4, ne^{-f(n)}) = o(n^2)\); that is, for every \(\epsilon > 0\) and all sufficiently large \(n\), every \(K_4\)-free graph on \(n\) vertices with independence number at most \(ne^{-f(n)}\) has at most \(\epsilon n^2\) edges.

theorem erdos_615.variants.sudakov (f : ℕ → ℝ)
    (hf : Tendsto (fun n : ℕ => f n / Real.sqrt (Real.log n)) atTop atTop)
    (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ (n : ℕ) in atTop,
      ∀ G : SimpleGraph (Fin n), G.CliqueFree 4 →
        (G.indepNum : ℝ) ≤ n * Real.exp (-f n) →
        (G.edgeFinset.card : ℝ) ≤ ε * n ^ 2

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/615.lean, line 96.

Sources

• FormalConjectures/ErdosProblems/615.lean at 2055e5ad
• erdosproblems.com/615

LeanErdos615.erdos_615 · Erdos615.erdos_615.variants.fox_loh_zhao · Erdos615.erdos_615.variants.sudakov

TheoremErdős Problem 616#

References: - erdosproblems.com/616 - [EHT91] Erdős, Paul and Hajnal, András and Tuza, Zsolt, Local constraints ensuring small representing sets. J. Combin. Theory Ser. A (1991), 78-84.

Quoted from FormalConjectures/ErdosProblems/616.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/616.

The file states 1 research or textbook statement: 1 open.

Erdos616.erdos_616

Open: stated without proof.

Let \(r\geq 3\). For an \(r\)-uniform hypergraph \(G\) let \(\tau(G)\) denote the covering number (or transversal number), the minimum size of a set of vertices which includes at least one from each edge in \(G\). Determine the best possible \(t\) such that, if \(G\) is an \(r\)-uniform hypergraph \(G\) where every subgraph \(G'\) on at most \(3r-3\) vertices has \(\tau(G')\leq 1\), we have \(\tau(G)\leq t\).

theorem erdos_616 :
    ∀ r : ℕ, 3 ≤ r → Hypergraph.localTransversalBound r (3 * r - 3) 1 = erdos_616.answer r

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/616.lean, line 44.

Sources

• FormalConjectures/ErdosProblems/616.lean at 2055e5ad
• erdosproblems.com/616

LeanErdos616.erdos_616

TheoremErdős Problem 617#

References: - erdosproblems.com/617 - [ErGy99] Erdős, Paul and Gyárfás, András, Split and balanced colorings of complete graphs. Discrete Math. (1999), 79-86.

Quoted from FormalConjectures/ErdosProblems/617.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/617.

The file states 4 research or textbook statements: 1 open and 3 solved.

Erdos617.erdos_617

Open: stated without proof.

Let \(r\geq 3\). If the edges of \(K_{r^2+1}\) are \(r\)-coloured then there exist \(r+1\) vertices with at least one colour missing on the edges of the induced \(K_{r+1}\).

In other words, there is no balanced colouring.

A conjecture of Erdős and Gyárfás [ErGy99].

theorem erdos_617 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
    (hV : Fintype.card V = r^2 + 1) (coloring : Sym2 V → Fin r) :
    ∃ (S : Finset V) (k : Fin r),
      S.card = r + 1 ∧
      ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/617.lean, line 42.

Erdos617.erdos_617.variants.r_eq_3

Solved: stated here without proof.

Erdős and Gyárfás [ErGy99] proved the conjecture for \(r=3\).

theorem erdos_617.variants.r_eq_3 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
    (hV : Fintype.card V = 3^2 + 1) (coloring : Sym2 V → Fin 3) :
    ∃ (S : Finset V) (k : Fin 3),
      S.card = 3 + 1 ∧
      ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/617.lean, line 53.

Erdos617.erdos_617.variants.r_eq_4

Solved: stated here without proof.

Erdős and Gyárfás [ErGy99] proved the conjecture for \(r=4\).

theorem erdos_617.variants.r_eq_4 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
    (hV : Fintype.card V = 4^2 + 1) (coloring : Sym2 V → Fin 4) :
    ∃ (S : Finset V) (k : Fin 4),
      S.card = 4 + 1 ∧
      ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/617.lean, line 64.

Erdos617.erdos_617.variants.r2

Solved: stated here without proof.

Erdős and Gyárfás [ErGy99] showed this property fails for infinitely many \(r\) if we replace \(r^2+1\) by \(r^2\).

theorem erdos_617.variants.r2 :
    {r : ℕ | ∃ (V : Type) (_ : Fintype V) (_ : DecidableEq V), Fintype.card V = r^2 ∧
      ∃ (coloring : Sym2 V → Fin r),
        ∀ (S : Finset V), S.card = r + 1 →
          ∀ (k : Fin r), ∃ u ∈ S, ∃ v ∈ S, u ≠ v ∧ coloring s(u, v) = k}.Infinite

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/617.lean, line 76.

Sources

• FormalConjectures/ErdosProblems/617.lean at 2055e5ad
• erdosproblems.com/617

LeanErdos617.erdos_617 · Erdos617.erdos_617.variants.r_eq_3 · Erdos617.erdos_617.variants.r_eq_4 · Erdos617.erdos_617.variants.r2

TheoremErdős Problem 618#

References: - erdosproblems.com/618 - [Er99] Erdős, Paul, A selection of problems and results in combinatorics. Combin. Probab. Comput. (1999), 1-6. - [EGR98] Erdős, Paul and Gyárfás, András and Ruszinkó, Miklós, How to decrease the diameter of triangle-free graphs. Combinatorica (1998), 493-501.

Quoted from FormalConjectures/ErdosProblems/618.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/618.

The file states 1 research or textbook statement: 1 solved.

Erdos618.erdos_618

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos618.lean.

For a triangle-free graph \(G\) let \(h_2(G)\) be the smallest number of edges that need to be added to \(G\) so that it has diameter \(2\) and is still triangle-free. Is it true that if \(G\) has maximum degree \(o(n^{1/2})\) then \(h(G)=o(n^2)\)?

A problem of Erdős, Gyárfás, and Ruszinkó [EGR98]. Simonovits showed that there exist graphs \(G\) with maximum degree \(\gg n^{1/2}\) and \(h_2(G)\gg n^2\). Alon has observed this problem is essentially identical to [134], and his solution in this note also solves this problem in the affirmative.

theorem erdos_618 :
    ∀ (G : ∀ n : ℕ, SimpleGraph (Fin n)),
      (∀ n, (G n).CliqueFree 3) →
      (fun n => ((G n).maxDegree : ℝ)) =o[atTop] (fun n => (n : ℝ) ^ ((1 : ℝ) / 2)) →
      (fun n => (h2 (G n) : ℝ)) =o[atTop] (fun n => (n : ℝ) ^ 2)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/618.lean, line 63.

Sources

• FormalConjectures/ErdosProblems/618.lean at 2055e5ad
• erdosproblems.com/618

LeanErdos618.erdos_618

TheoremErdős Problem 619#

References: - erdosproblems.com/619 - [EGR98] Erdős, Paul and Gyárfás, András and Ruszinkó, Miklós, How to decrease the diameter of triangle-free graphs. Combinatorica 18 (1998), 493-501. - [Er99] Erdős, Paul, A selection of problems and results in combinatorics. Combin. Probab. Comput. 8 (1999), 1-6.

Quoted from FormalConjectures/ErdosProblems/619.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/619.

The file states 5 research or textbook statements: 5 solved. It also has 2 test statements, counted here but not shown.

Erdos619.erdos_619

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/b8c7a76f267c29eaa41d1212c211a920be8b05ea/FormalConjectures/ErdosProblems/619.lean#L6009; a Lean proof is at https://github.com/nick-kuhn/erdos-619/blob/7f65718b8c1019ecc24e6c9a6b04ec4c66a4e26f/Solution.lean#L5869.

Erdős Problem 619 [EGR98, Er99]: For a triangle-free graph \(G\) let \(h_r(G)\) be the smallest number of edges that need to be added to \(G\) so that it has diameter \(r\) (while preserving the property of being triangle-free). Is it true that there exists a constant \(c>0\) such that if \(G\) is a connected graph on \(n\) vertices then \(h_4(G)<(1-c)n\)?

The answer is no: for every \(\eta>0\) there exist connected triangle-free graphs on \(n\) vertices with \(h_4(G)\geq(1-\eta)n\), so no such constant \(c\) exists. The original proof was generated by Claude Fable 5; the Lean formalization was sketched by Fable and implemented by GPT 5.5 with Codex (see the linked formal_proof).

theorem erdos_619 :
    ¬ ∃ c > (0 : ℝ), ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
      G.Connected → G.CliqueFree 3 →
      (minNewEdges 4 G : ℝ) < (1 - c) * Fintype.card V

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/619.lean, line 71.

Erdos619.erdos_619.variants.add_edges_diam_three

Solved: stated here without proof.

Erdős, Gyárfás and Ruszinkó [EGR98]: every connected triangle-free graph on a finite vertex set can be extended, by adding edges, to a triangle-free graph of diameter at most \(3\). This shows that the infimum defining minNewEdges r G ranges over a nonempty set for every 3 ≤ r.

theorem erdos_619.variants.add_edges_diam_three {V : Type*} [Fintype V]
    (G : SimpleGraph V) (hG : G.Connected) (hG' : G.CliqueFree 3) :
    ∃ H : SimpleGraph V, G ≤ H ∧ H.CliqueFree 3 ∧ H.ediam ≤ 3

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/619.lean, line 88.

Erdos619.erdos_619.variants.h_three_le

Solved: stated here without proof.

Erdős, Gyárfás and Ruszinkó [EGR98]: \(h_3(G) \leq n\) for every connected triangle-free graph \(G\) on \(n\) vertices.

theorem erdos_619.variants.h_three_le {V : Type*} [Fintype V]
    (G : SimpleGraph V) (hG : G.Connected) (hG' : G.CliqueFree 3) :
    minNewEdges 3 G ≤ Fintype.card V

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/619.lean, line 98.

Erdos619.erdos_619.variants.h_five_le

Solved: stated here without proof.

Erdős, Gyárfás and Ruszinkó [EGR98]: \(h_5(G) \leq \frac{n-1}{2}\) for every connected triangle-free graph \(G\) on \(n\) vertices.

theorem erdos_619.variants.h_five_le {V : Type*} [Fintype V]
    (G : SimpleGraph V) (hG : G.Connected) (hG' : G.CliqueFree 3) :
    (minNewEdges 5 G : ℝ) ≤ (Fintype.card V - 1) / 2

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/619.lean, line 108.

Erdos619.erdos_619.variants.h_three_lower

Solved: stated here without proof.

Erdős, Gyárfás and Ruszinkó [EGR98]: there is a constant \(c > 0\) such that for every \(n\) there exist connected triangle-free graphs \(G\) on \(n\) vertices with \(h_3(G) \geq n - c\).

theorem erdos_619.variants.h_three_lower :
    ∃ c > (0 : ℝ), ∀ n : ℕ, 0 < n →
      ∃ (V : Type) (_ : Fintype V) (G : SimpleGraph V),
        Fintype.card V = n ∧ G.Connected ∧ G.CliqueFree 3 ∧
        (n : ℝ) - c ≤ minNewEdges 3 G

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/619.lean, line 119.

Sources

• FormalConjectures/ErdosProblems/619.lean at 2055e5ad
• erdosproblems.com/619

LeanErdos619.erdos_619 · Erdos619.erdos_619.variants.add_edges_diam_three · Erdos619.erdos_619.variants.h_three_le · Erdos619.erdos_619.variants.h_five_le · Erdos619.erdos_619.variants.h_three_lower

TheoremErdős Problem 621#

References: - erdosproblems.com/621 - [EGT96] Erdős, Paul and Gallai, Tibor and Tuza, Zsolt, Covering and independence in triangle structures. Discrete Math. (1996), 89-101. - [Er99] Erdős, Paul, A selection of problems and results in combinatorics. Combin. Probab. Comput. (1999), 1-6. - [NoSu16] S. Norin and Y.-R. Sun, Triangle-free independent sets vs. cuts. arXiv:1602.04370 (2016).

Quoted from FormalConjectures/ErdosProblems/621.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/621.

The file states 1 research or textbook statement: 1 solved.

Erdos621.erdos_621

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos621.lean.

Let \(G\) be a graph on \(n\) vertices, \(\alpha_1(G)\) be the maximum number of edges that contain at most one edge from every triangle, and \(\tau_1(G)\) be the minimum number of edges that contain at least one edge from every triangle.

Is it true that

\[\alpha_1(G)+\tau_1(G) \leq \frac{n^2}{4}?\]

A problem of Erdős, Gallai, and Tuza [EGT96], who observe that this is probably quite difficult since there are different examples where equality hold: the complete graph, the complete bipartite graph, and the graph obtained from \(K_{m,m}\) by adding one vertex joined to every other.

This is true, and was proved by Norin and Sun [NoSu16], who in fact proved that

\[\alpha_1(G)+\tau_B(G) \leq \frac{n^2}{4},\]

where \(\tau_B(G)\) is the minimum number of edges that need to be removed to make the graph bipartite.

Here \(\alpha_1(G)\) and \(\tau_1(G)\) are taken over subsets of the edge set of \(G\), and the inequality is stated multiplied through by \(4\) so that it lives in the natural numbers.

The linked file states \(\tau_1\) as the least number of edges whose deletion leaves \(G\) triangle-free, which is the same as meeting every triangle of \(G\), and quantifies over an arbitrary Fintype V rather than Fin n.

theorem erdos_621 :
    ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (a t : ℕ),
      IsGreatest {k : ℕ | ∃ A ⊆ G.edgeFinset, A.card = k ∧
        ∀ x y z : Fin n, G.Adj x y → G.Adj y z → G.Adj x z →
          (({s(x, y), s(y, z), s(x, z)} : Finset (Sym2 (Fin n))) ∩ A).card ≤ 1} a →
      IsLeast {k : ℕ | ∃ T ⊆ G.edgeFinset, T.card = k ∧
        ∀ x y z : Fin n, G.Adj x y → G.Adj y z → G.Adj x z →
          (T ∩ ({s(x, y), s(y, z), s(x, z)} : Finset (Sym2 (Fin n)))).Nonempty} t →
      4 * (a + t) ≤ n ^ 2

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/621.lean, line 65.

Sources

• FormalConjectures/ErdosProblems/621.lean at 2055e5ad
• erdosproblems.com/621

LeanErdos621.erdos_621

TheoremErdős Problem 623#

Reference: erdosproblems.com/623

Quoted from FormalConjectures/ErdosProblems/623.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/623.

The file states 1 research or textbook statement: 1 open.

Erdos623.erdos_623

Open: stated without proof.

Let \(X\) be a set of cardinality \(\aleph_\omega\) and \(f\) be a function from the finite subsets of \(X\) to \(X\) such that \(f(A)\not\in A\) for all \(A\). Must there exist an infinite \(Y\subseteq X\) that is independent - that is, for all finite \(B\subset Y\) we have \(f(B)\not\in Y\)?

theorem erdos_623 : ∀ (X : Type u) (hX : #X = ℵ_ ω)
    (f : Finset X → X), (∀ A : Finset X, f A ∉ A) →
    (∃ Y : Set X, Set.Infinite Y ∧ (∀ (B : Finset X), ↑B ⊆ Y → f B ∉ Y))

Category research open; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/623.lean, line 39.

Sources

• FormalConjectures/ErdosProblems/623.lean at 2055e5ad
• erdosproblems.com/623

LeanErdos623.erdos_623

TheoremErdős Problem 624#

Reference: erdosproblems.com/624

Quoted from FormalConjectures/ErdosProblems/624.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/624.

The file states 1 research or textbook statement: 1 open.

Erdos624.erdos_624

Open: stated without proof.

Let \(X\) be a finite set of size \(n\) and \(H(n)\) be such that there is a function \(f:\{A : A\subseteq X\}\to X\) so that for every \(Y\subseteq X\) with \(\lvert Y\rvert \geq H(n)\) we have \(\left\{ f(A) : A\subseteq Y\right\}=X\). Prove that \(H(n)-\log_2 n \to \infty\).

theorem erdos_624 :
    atTop.Tendsto (fun n : ℕ => H n - Real.logb 2 (n : ℝ)) atTop

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/624.lean, line 60.

Sources

• FormalConjectures/ErdosProblems/624.lean at 2055e5ad
• erdosproblems.com/624

LeanErdos624.erdos_624

TheoremErdős Problem 626#

References: - erdosproblems.com/626 - [Er59b] Erdős, P., Graph theory and probability. Canadian J. Math. (1959), 34-38. - [Er62b] Erdős, P., On circuits and subgraphs of chromatic graphs. Mathematika (1962), 170-175. - [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35. - [Ko88] Kostochka, A. V., Upper bounds on the chromatic number of graphs. Trudy Inst. Mat. (Novosibirsk) (1988), 204-226, 265.

Quoted from FormalConjectures/ErdosProblems/626.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/626.

The file states 8 research or textbook statements: 4 open and 4 solved. It also has 1 test statement, counted here but not shown.

Erdos626.erdos_626.parts.i

Open: stated without proof.

Let \(k \geq 4\) and let \(g_k(n)\) denote the largest \(m\) such that there is a graph on \(n\) vertices with chromatic number \(k\) and girth \(> m\) (i.e. containing no cycle of length \(\leq m\)). Does

\[\lim_{n\to\infty}\frac{g_k(n)}{\log n}\]

exist?

By Erdos626.erdos_626.variants.kostochka and Erdos626.erdos_626.variants.erdos_upper, the limit, if it exists, is a positive real number.

theorem erdos_626.parts.i :
    ∀ k : ℕ, 4 ≤ k → ∃ L : ℝ,
      Tendsto (fun n : ℕ ↦ (g k n : ℝ) / Real.log n) atTop (𝓝 L)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/626.lean, line 85.

Erdos626.erdos_626.variants.kostochka

Solved: stated here without proof.

Kostochka [Ko88] proved that for \(k \geq 4\)

\[g_k(n) \geq \frac{1}{4\log k}\log n.\]

Kostochka's theorem gives this lower bound for the girth itself, and \(g_k(n)\) is one less than the largest possible girth, so the inequality above holds only up to \(1\). The statement below is a consequence of his theorem, not the theorem itself: for every \(\varepsilon > 0\) and all sufficiently large \(n\), \(g_k(n) \geq \left(\frac{1}{4\log k} - \varepsilon\right)\log n\).

theorem erdos_626.variants.kostochka :
    ∀ k : ℕ, 4 ≤ k → ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (1 / (4 * Real.log k) - ε) * Real.log n ≤ (g k n : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/626.lean, line 99.

Erdos626.erdos_626.variants.erdos_upper

Solved: stated here without proof.

Erdős [Er59b] proved that for \(k \geq 4\)

\[g_k(n) \leq \frac{2}{\log(k-2)}\log n + 1.\]

We state it for all sufficiently large \(n\).

theorem erdos_626.variants.erdos_upper :
    ∀ k : ℕ, 4 ≤ k → ∀ᶠ n : ℕ in atTop,
      (g k n : ℝ) ≤ 2 * Real.log n / Real.log ((k : ℝ) - 2) + 1

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/626.lean, line 110.

Erdos626.erdos_626.parts.ii

Open: stated without proof.

Let \(h^{(m)}(n)\) be the maximal chromatic number of a graph on \(n\) vertices with girth \(> m\). Does

\[\lim_{n\to\infty}\frac{\log h^{(m)}(n)}{\log n}\]

exist, and what is its value? The value is asked for in Erdos626.erdos_626.variants.h_odd_conjecture and Erdos626.erdos_626.variants.h_even_conjecture.

theorem erdos_626.parts.ii :
    ∀ m : ℕ, ∃ L : ℝ,
      Tendsto (fun n : ℕ ↦ Real.log (h m n : ℝ) / Real.log n) atTop (𝓝 L)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/626.lean, line 123.

Erdos626.erdos_626.variants.h_lower

Solved: stated here without proof.

Erdős [Er59b] proved that

\[\lim_{n\to\infty}\frac{\log h^{(m)}(n)}{\log n} \gg \frac{1}{m}.\]

The existence of the limit is open, so we state the lower bound for the lower limit: there is an absolute constant \(c > 0\) such that for every \(m \geq 1\) and \(\varepsilon > 0\), eventually \(h^{(m)}(n) \geq n^{c/m - \varepsilon}\).

theorem erdos_626.variants.h_lower :
    ∃ c > (0 : ℝ), ∀ m : ℕ, 1 ≤ m → ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (n : ℝ) ^ (c / (m : ℝ) - ε) ≤ (h m n : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/626.lean, line 136.

Erdos626.erdos_626.variants.h_upper_odd

Solved: stated here without proof.

Erdős [Er59b] proved that for odd \(m\)

\[\lim_{n\to\infty}\frac{\log h^{(m)}(n)}{\log n} \leq \frac{2}{m+1}.\]

The existence of the limit is open, so we state the bound for the upper limit: for every \(\varepsilon > 0\), eventually \(h^{(m)}(n) \leq n^{2/(m+1) + \varepsilon}\).

theorem erdos_626.variants.h_upper_odd :
    ∀ m : ℕ, Odd m → ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (h m n : ℝ) ≤ (n : ℝ) ^ (2 / ((m : ℝ) + 1) + ε)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/626.lean, line 148.

Erdos626.erdos_626.variants.h_odd_conjecture

Open: stated without proof.

Erdős conjectured that the bound in Erdos626.erdos_626.variants.h_upper_odd is sharp: for odd \(m\),

\[\lim_{n\to\infty}\frac{\log h^{(m)}(n)}{\log n} = \frac{2}{m+1}.\]

theorem erdos_626.variants.h_odd_conjecture :
    ∀ m : ℕ, Odd m → Tendsto (fun n : ℕ ↦ Real.log (h m n : ℝ) / Real.log n) atTop
      (𝓝 (2 / ((m : ℝ) + 1)))

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/626.lean, line 159.

Erdos626.erdos_626.variants.h_even_conjecture

Open: stated without proof.

For even \(m\), Erdős had no good guess for the value of the limit, other than that it should lie in \(\left[\frac{2}{m+2}, \frac{2}{m}\right]\). He could not prove this even for \(m = 4\).

The existence of the limit is open, so we state the claim for the lower and upper limits: for every \(\varepsilon > 0\), eventually \(n^{2/(m+2) - \varepsilon} \leq h^{(m)}(n) \leq n^{2/m + \varepsilon}\). We require \(m \geq 2\), since \(2/m\) is undefined for \(m = 0\). The upper half is known: girth \(> m\) implies girth \(> m - 1\), so \(h^{(m)}(n) \leq h^{(m-1)}(n)\), and Erdos626.erdos_626.variants.h_upper_odd for the odd number \(m - 1\) gives the exponent \(2/m\).

theorem erdos_626.variants.h_even_conjecture :
    ∀ m : ℕ, Even m → 2 ≤ m → ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (n : ℝ) ^ (2 / ((m : ℝ) + 2) - ε) ≤ (h m n : ℝ) ∧
        (h m n : ℝ) ≤ (n : ℝ) ^ (2 / (m : ℝ) + ε)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/626.lean, line 176.

Sources

• FormalConjectures/ErdosProblems/626.lean at 2055e5ad
• erdosproblems.com/626

LeanErdos626.erdos_626.parts.i · Erdos626.erdos_626.variants.kostochka · Erdos626.erdos_626.variants.erdos_upper · Erdos626.erdos_626.parts.ii · Erdos626.erdos_626.variants.h_lower · Erdos626.erdos_626.variants.h_upper_odd · Erdos626.erdos_626.variants.h_odd_conjecture · Erdos626.erdos_626.variants.h_even_conjecture

TheoremErdős Problem 627#

References: - erdosproblems.com/627 - [AFM25] Araujo, I. and Filipe, R. and Miyazaki, R., A note on the maximum ratio between chromatic number and clique number. arXiv:2512.16062 (2025). - [Er61d] Erdős, P., Graph theory and probability. II. Canadian J. Math. (1961), 346-352. - [Er67c] Erdős, P., Some remarks on chromatic graphs. Colloq. Math. (1967), 253-256. - [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35. - [My55] Mycielski, J., Sur le coloriage des graphs. Colloquium Mathematicum 3 (1955), 161–162. doi:10.4064/cm-3-2-161-162 - [Zy52] Zykov, A. A., On some properties of linear complexes. Amer. Math. Soc. Translation (1952), 33.

Quoted from FormalConjectures/ErdosProblems/627.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/627.

The file states 9 research or textbook statements: 1 open and 8 solved.

Erdos627.erdos_627

Open: stated without proof.

Let \(\omega(G)\) denote the clique number of \(G\) and \(\chi(G)\) the chromatic number. If \(f(n)\) is the maximum value of \(\chi(G)/\omega(G)\), as \(G\) ranges over all graphs on \(n\) vertices, then does

\[\lim_{n\to\infty}\frac{f(n)}{n/(\log_2n)^2}\]

exist?

Since \(f(n) \asymp n/(\log_2 n)^2\) (see Erdos627.erdos_627.variants.theta), the limit, if it exists, is a finite real number.

theorem erdos_627 :
    ∃ L : ℝ, Tendsto (fun n : ℕ ↦ maxChromaticCliqueRatio n / ((n : ℝ) / Real.logb 2 n ^ 2))
      atTop (𝓝 L)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/627.lean, line 67.

Erdos627.erdos_627.variants.theta

Solved: stated here without proof.

Erdős [Er67c] proved that

\[f(n) \asymp \frac{n}{(\log_2 n)^2}.\]

theorem erdos_627.variants.theta :
    (fun n : ℕ ↦ maxChromaticCliqueRatio n) =Θ[atTop]
      (fun n : ℕ ↦ (n : ℝ) / Real.logb 2 n ^ 2)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/627.lean, line 77.

Erdos627.erdos_627.variants.lower

Solved: stated here without proof.

Erdős [Er67c] proved the lower bound

\[f(n) \geq \left(\frac{1}{4} + o(1)\right) \frac{n}{(\log_2 n)^2}.\]

theorem erdos_627.variants.lower :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (1 / 4 - ε) * ((n : ℝ) / Real.logb 2 n ^ 2) ≤ maxChromaticCliqueRatio n

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/627.lean, line 87.

Erdos627.erdos_627.variants.upper

Solved: stated here without proof.

The method of Erdős [Er67c] gives the upper bound

\[f(n) \leq (4 + o(1)) \frac{n}{(\log_2 n)^2}.\]

Erdős states the constant as \(1\), but Araujo, Filipe, and Miyazaki [AFM25] note that his method gives \(4\).

theorem erdos_627.variants.upper :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      maxChromaticCliqueRatio n ≤ (4 + ε) * ((n : ℝ) / Real.logb 2 n ^ 2)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/627.lean, line 99.

Erdos627.erdos_627.variants.limit_bounds

Solved: stated here without proof.

Consequently, if the limit in Erdos627.erdos_627 exists, it lies in \([1/4, 4]\) [Er67c] (with the correction of the upper constant from \(1\) to \(4\) noted in [AFM25]).

theorem erdos_627.variants.limit_bounds :
    ∀ L : ℝ, Tendsto (fun n : ℕ ↦ maxChromaticCliqueRatio n / ((n : ℝ) / Real.logb 2 n ^ 2))
      atTop (𝓝 L) → 1 / 4 ≤ L ∧ L ≤ 4

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/627.lean, line 109.

Erdos627.erdos_627.variants.afm_upper

Solved: stated here without proof.

Araujo, Filipe, and Miyazaki [AFM25, Theorem 1.3] improved the upper bound to

\[f(n) \leq (3.71943 + o(1)) \frac{n}{(\log_2 n)^2},\]

using recent improvements in the asymptotics of Ramsey numbers. [AFM25] is an arXiv preprint.

theorem erdos_627.variants.afm_upper :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      maxChromaticCliqueRatio n ≤ (3.71943 + ε) * ((n : ℝ) / Real.logb 2 n ^ 2)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/627.lean, line 120.

Erdos627.erdos_627.variants.conditional

Solved: stated here without proof.

Araujo, Filipe, and Miyazaki [AFM25, Theorem 1.2]: suppose that \(R(s,t) \leq R(k)\) for all \(s, t, k \in \mathbb{N}\) with \(st \leq k^2\) (their Conjecture 1.1), and that \(\lim_{k \to \infty} \frac{\log_2 R(k)}{k}\) exists and equals \(\ell\). Then

\[f(n) = (\ell^2 + o(1)) \frac{n}{(\log_2 n)^2},\]

so the limit in Erdos627.erdos_627 exists and equals \(\ell^2\). Here \(R(s,t)\) is the two-colour Ramsey number and \(R(k) = R(k,k)\) (see [77]). [AFM25] is an arXiv preprint.

theorem erdos_627.variants.conditional (ℓ : ℝ)
    (hR : ∀ s t k : ℕ, s * t ≤ k ^ 2 → classicalRamsey s t ≤ diagonalRamsey k)
    (hlim : Tendsto (fun k : ℕ ↦ Real.logb 2 (diagonalRamsey k : ℝ) / (k : ℝ)) atTop (𝓝 ℓ)) :
    Tendsto (fun n : ℕ ↦ maxChromaticCliqueRatio n / ((n : ℝ) / Real.logb 2 n ^ 2))
      atTop (𝓝 (ℓ ^ 2))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/627.lean, line 134.

Erdos627.erdos_627.variants.tutte_zykov

Proved here.

Tutte and Zykov [Zy52] independently proved that for every \(k\) there is a graph with \(\omega(G) = 2\) and \(\chi(G) = k\).

We require \(k \geq 2\): a graph with \(\omega(G) = 2\) has an edge, so \(\chi(G) \geq 2\). The proof here uses Mycielski's construction [My55].

theorem erdos_627.variants.tutte_zykov :
    ∀ k : ℕ, 2 ≤ k → ∃ (n : ℕ) (G : SimpleGraph (Fin n)),
      G.cliqueNum = 2 ∧ G.chromaticNumber = (k : ℕ∞)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/627.lean, line 149.

Erdos627.erdos_627.variants.erdos_1961

Solved: stated here without proof.

Erdős [Er61d] proved that for every (large) \(n\) there is a graph on \(n\) vertices with \(\omega(G) = 2\) and

\[\chi(G) \gg \frac{n^{1/2}}{\log n},\]

whence \(f(n) \gg n^{1/2}/\log n\).

theorem erdos_627.variants.erdos_1961 :
    ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∃ G : SimpleGraph (Fin n),
      G.cliqueNum = 2 ∧
        c * Real.sqrt (n : ℝ) / Real.log (n : ℝ) ≤ (G.chromaticNumber.toNat : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/627.lean, line 161.

Sources

• FormalConjectures/ErdosProblems/627.lean at 2055e5ad
• erdosproblems.com/627

LeanErdos627.erdos_627 · Erdos627.erdos_627.variants.theta · Erdos627.erdos_627.variants.lower · Erdos627.erdos_627.variants.upper · Erdos627.erdos_627.variants.limit_bounds · Erdos627.erdos_627.variants.afm_upper · Erdos627.erdos_627.variants.conditional · Erdos627.erdos_627.variants.tutte_zykov · Erdos627.erdos_627.variants.erdos_1961

TheoremErdős Problem 628#

References: - erdosproblems.com/628 - [BKPS09] Balogh, József and Kostochka, Alexandr V. and Prince, Noah and Stiebitz, Michael, The Erdős-Lovász Tihany conjecture for quasi-line graphs. Discrete Math. (2009), 3985-3991. - [BrJu69] Brown, W. G. and Jung, H. A., On odd circuits in chromatic graphs. Acta Math. Acad. Sci. Hungar. (1969), 129-134. - [Er68b] Erdős, P., Problem 2. Theory of Graphs (1968), 361. - [So22] Song, Zi-Xia, A survey on the Erdős-Lovász Tihany conjecture. Adv. Math. (China) (2022), 259--274.

Quoted from FormalConjectures/ErdosProblems/628.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/628.

The file states 4 research or textbook statements: 1 open and 3 solved.

Erdos628.erdos_628

Open: stated without proof.

Let \(G\) be a graph with chromatic number \(k\) containing no \(K_k\). If \(a,b\geq 2\) and \(a+b=k+1\) then must there exist two disjoint subgraphs of \(G\) with chromatic numbers \(\geq a\) and \(\geq b\) respectively?

theorem erdos_628 (V : Type*) [Fintype V] (G : SimpleGraph V) (k : ℕ)
    (hG_chrom : G.chromaticNumber = (k : ℕ∞))
    (hG_clique : G.CliqueFree k)
    (a b : ℕ) (ha : a ≥ 2) (hb : b ≥ 2) (hab : a + b = k + 1) :
    ∃ (s : Set V),
      (G.induce s).chromaticNumber ≥ (a : ℕ∞) ∧
      (G.induce sᶜ).chromaticNumber ≥ (b : ℕ∞)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/628.lean, line 46.

Erdos628.erdos_628.variants.k_5_a_3_b_3

Solved: stated here without proof.

Erdős [Er68b] originally asked about \(a=b=3\) which was proved by Brown and Jung [BrJu69] (who in fact prove that \(G\) must contain two vertex disjoint odd cycles)..

theorem erdos_628.variants.k_5_a_3_b_3 (V : Type*) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hG_chrom : G.chromaticNumber = (5 : ℕ∞))
    (hG_clique : G.CliqueFree 5) :
    ∃ (s : Set V),
      (G.induce s).chromaticNumber ≥ (3 : ℕ∞) ∧
      (G.induce sᶜ).chromaticNumber ≥ (3 : ℕ∞)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/628.lean, line 61.

Erdos628.erdos_628.variants.quasi_line

Solved: stated here without proof.

Balogh, Kostochka, Prince, and Stiebitz [BKPS09] proved the conjecture for quasi-line graphs.

theorem erdos_628.variants.quasi_line (V : Type*) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hG_quasi : IsQuasiLineGraph G)
    (k : ℕ)
    (hG_chrom : G.chromaticNumber = (k : ℕ∞))
    (hG_clique : G.CliqueFree k)
    (a b : ℕ) (ha : a ≥ 2) (hb : b ≥ 2) (hab : a + b = k + 1) :
    ∃ (s : Set V),
      (G.induce s).chromaticNumber ≥ (a : ℕ∞) ∧
      (G.induce sᶜ).chromaticNumber ≥ (b : ℕ∞)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/628.lean, line 73.

Erdos628.erdos_628.variants.independence_number_2

Solved: stated here without proof.

Balogh, Kostochka, Prince, and Stiebitz [BKPS09] proved the conjecture for graphs with independence number 2.

theorem erdos_628.variants.independence_number_2 (V : Type*) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hG_indep : G.indepNum = 2)
    (k : ℕ)
    (hG_chrom : G.chromaticNumber = (k : ℕ∞))
    (hG_clique : G.CliqueFree k)
    (a b : ℕ) (ha : a ≥ 2) (hb : b ≥ 2) (hab : a + b = k + 1) :
    ∃ (s : Set V),
      (G.induce s).chromaticNumber ≥ (a : ℕ∞) ∧
      (G.induce sᶜ).chromaticNumber ≥ (b : ℕ∞)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/628.lean, line 88.

Sources

• FormalConjectures/ErdosProblems/628.lean at 2055e5ad
• erdosproblems.com/628

LeanErdos628.erdos_628 · Erdos628.erdos_628.variants.k_5_a_3_b_3 · Erdos628.erdos_628.variants.quasi_line · Erdos628.erdos_628.variants.independence_number_2

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.