Erdős Problem 579 to Erdős Problem 599

TheoremErdős Problem 579#

References: - erdosproblems.com/579 - [EHSS83] P. Erdős, A. Hajnal, V. T. Sós and E. Szemerédi, More results on Ramsey–Turán type problems, Combinatorica 3 (1983), 69–81.

Quoted from FormalConjectures/ErdosProblems/579.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/579.

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

Erdos579.erdos_579

Open: stated without proof.

Let \(\delta > 0\). If \(n\) is sufficiently large and \(G\) is a graph on \(n\) vertices with no \(K_{2,2,2}\) (the octahedron) and at least \(\delta n^2\) edges, must \(G\) contain an independent set of size \(\gg_\delta n\)?

This is a problem of Erdős, Hajnal, Sós, and Szemerédi [EHSS83]. It is open; they proved the statement for \(\delta > 1/8\) (see erdos_579.variants.ehss_large_delta), and the difficulty is to push the edge-density threshold down to an arbitrary \(\delta > 0\).

Here \(K_{2,2,2}\) is the complete tripartite graph with all parts of size \(2\), encoded as completeMultipartiteGraph (fun _ : Fin 3 => Fin 2); "contains no \(K_{2,2,2}\)" is expressed via SimpleGraph.Free.

theorem erdos_579 :
    ∀ δ : ℝ, 0 < δ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
      ∀ G : SimpleGraph (Fin n), octahedron.Free G →
        δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
          c * n ≤ (G.indepNum : ℝ)

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

Erdos579.erdos_579.variants.ehss_large_delta

Solved: stated here without proof.

The partial result of Erdős, Hajnal, Sós, and Szemerédi [EHSS83]: the statement of erdos_579 holds whenever the edge-density coefficient exceeds \(1/8\). That is, for every \(\delta > 1/8\) there is a \(c > 0\) such that for all sufficiently large \(n\), every \(K_{2,2,2}\)-free graph \(G\) on \(n\) vertices with at least \(\delta n^2\) edges has an independent set of size at least \(c n\).

theorem erdos_579.variants.ehss_large_delta (δ : ℝ) (hδ : 1 / 8 < δ) :
    ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
      ∀ G : SimpleGraph (Fin n), octahedron.Free G →
        δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
          c * n ≤ (G.indepNum : ℝ)

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

Sources
LeanErdos579.erdos_579 · Erdos579.erdos_579.variants.ehss_large_delta

TheoremErdős Problem 581#

References: - erdosproblems.com/581 - [CEG79] Chung, F. R. K. and Erdős, P. and Graham, R. L., On the product of the point and line covering numbers of a graph. Second International Conference on Combinatorial Mathematics (New York, 1978) (1979), 597-602. - [Al96] Alon, Noga, Bipartite subgraphs. Combinatorica (1996), 301-311.

Quoted from FormalConjectures/ErdosProblems/581.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/581.

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

Erdos581.erdos_581

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos581.lean#L31.

Let \(f(m)\) be the maximal \(k\) such that a triangle-free graph on \(m\) edges must contain a bipartite graph with \(k\) edges. Determine \(f(m)\).

Resolved by Alon [Al96], who showed that there exist constants \(c_1,c_2>0\) such that

\[\frac{m}{2}+c_1m^{4/5}\leq f(m)\leq \frac{m}{2}+c_2m^{4/5}.\]
theorem erdos_581 : ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ ∀ m : ℕ,
    (m : ℝ) / 2 + c₁ * (m : ℝ) ^ (4 / 5 : ℝ) ≤ f m ∧
      (f m : ℝ) ≤ (m : ℝ) / 2 + c₂ * (m : ℝ) ^ (4 / 5 : ℝ)

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

Sources
LeanErdos581.erdos_581

TheoremErdős Problem 582#

References: - erdosproblems.com/582 - [Er75b] Erdős, Paul, Problems and results in combinatorial number theory. Journées Arithmétiques de Bordeaux (Conf., Univ. Bordeaux, Bordeaux, 1974) (1975), 295-310. - [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. - [Er75d] Erdős, Paul, Problems and results on finite and infinite graphs. Recent advances in graph theory (Proc. Second Czechoslovak Sympos., Prague, 1974) (1975), 183-192. (loose errata). - [FrRo86] Frankl, P. and Rödl, V., Large triangle-free subgraphs in graphs without {\(K_4\)}. Graphs Combin. (1986), 135-144. - [Sp88] Spencer, Joel, Three hundred million points suffice. J. Combin. Theory Ser. A (1988), 210-217. - [Lu07] Lu, Linyuan, Explicit construction of small Folkman graphs. SIAM J. Discrete Math. (2007), 1053-1060. - [DuRo08] Dudek, Andrzej and Rödl, Vojtěch, On the Folkman number {\(f(2,3,4)\)}. Experiment. Math. (2008), 63-67. - [RaXu07] Radziszowski, Stanisław P. and Xu, Xiaodong, On the most wanted Folkman graph. Geombinatorics (2007), 367-381. - [BiNe20] Bikov, Aleksandar and Nenov, Nedyalko, On the independence number of \((3,3)\)-Ramsey graphs and the Folkman number \(F_e(3,3;4)\). Australas. J. Combin. (2020), 35-50. - [ErHa67] Erdős, P. and Hajnal, A., Research Problem 2.5. J. Comb. Theory (1967). - [Fo70] Folkman, Jon, Graphs with monochromatic complete subgraphs in every edge coloring. SIAM J. Appl. Math. (1970), 19-24. - [LRX14] Lange, Alexander R. and Radziszowski, Stanisław P. and Xu, Xiaodong, Use of MAX-CUT for Ramsey arrowing of triangles. J. Combin. Math. Combin. Comput. (2014), 61-71.

Quoted from FormalConjectures/ErdosProblems/582.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/582.

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

Erdos582.erdos_582

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

Does there exist a graph \(G\) which contains no \(K_4\), and yet any \(2\)-colouring of the edges produces a monochromatic \(K_3\)?

Erdős and Hajnal [ErHa67] first asked for the existence of any such graph. Existence was proved by Folkman [Fo70], but with very poor quantitative bounds. (As a result these quantities are often called Folkman numbers.) The current best bounds on the minimal number of vertices \(N\) of such a graph are \(21 \leq N \leq 786\), where the lower bound is due to Bikov and Nenov [BiNe20] and the upper bound is due to Lange, Radziszowski, and Xu [LRX14].

theorem erdos_582 :
    ∃ (V : Type*) (_ : Fintype V) (G : SimpleGraph V),
      G.CliqueFree 4 ∧ EdgeRamseyTriangle G

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

Sources
LeanErdos582.erdos_582

TheoremErdős Problem 583#

References: - erdosproblems.com/583 - [AnBa23] Anto, Nevil and Basavaraju, Manu, Gallai's path decomposition for 2-degenerate graphs. Discrete Math. Theor. Comput. Sci. (2023), Paper No. 16, 11. - [BBB21] A. Blanché, M. Bonamy, and N. Bonichon, Gallai's path decomposition in planar graphs. arXiv:2110.08870 (2021). - [BoPe19] Bonamy, Marthe and Perrett, Thomas J., Gallai's path decomposition conjecture for graphs of small maximum degree. Discrete Math. (2019), 1293--1299. - [CFZ26] Chu, Yanan and Fan, Genghua and Zhou, Chuixiang, Gallai's conjecture and the path number of odd semi-cliques. Discrete Math. (2026), Paper No. 114725, 6. - [Ch78] Chung, F. R. K., On partitions of graphs into trees. Discrete Math. (1978), 23-30. - [DeKo00] Dean, Nathaniel and Kouider, Mekkia, Gallai's conjecture for disconnected graphs. Discrete Math. (2000), 43--54. - [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109. - [Fa02] Fan, Genghua, Subgraph coverings and edge switchings. J. Combin. Theory Ser. B (2002), 54-83. - [Lo68] Lovász, L., On covering of graphs. Theory of Graphs (Proc. Colloq., Tihany, 1966) (1968), 231-236. - [Py96] Pyber, L., Covering the edges of a connected graph by paths. J. Combin. Theory Ser. B (1996), 152-159.

Quoted from FormalConjectures/ErdosProblems/583.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/583.

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

Erdos583.erdos_583

Open: stated without proof.

Every connected graph on \(n\) vertices can be partitioned into at most \(\lceil n/2\rceil\) edge-disjoint paths.

A problem of Erdős and Gallai.

theorem erdos_583 {V : Type*} [Fintype V] (G : SimpleGraph V) (hG : G.Connected) :
    ∃ D : Finset G.Subgraph,
      (∀ H ∈ D, IsPathSubgraph H) ∧
      IsDecomposition G D ∧
      D.card ≤ ⌈(Fintype.card V : ℚ) / 2⌉₊

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

Sources
LeanErdos583.erdos_583

TheoremErdős Problem 586#

References: - erdosproblems.com/586 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er96b] Erdős, Paul, Some problems I presented or planned to present in my short talk. Analytic number theory, Vol. 1 (Allerton Park, IL, 1995) (1996), 333-335. - [Er97] Erdős, Paul, Problems in number theory. New Zealand J. Math. (1997), 155-160. - [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. - [BBMST22] Balister, Paul and Bollobás, Béla and Morris, Robert and Sahasrabudhe, Julian and Tiba, Marius, On the Erdős covering problem: the density of the uncovered set. Invent. Math. (2022), 377-414.

Quoted from FormalConjectures/ErdosProblems/586.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/586.

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

Erdos586.erdos_586

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos586.lean#L186.

Is there a covering system such that no two of the moduli divide each other?

Asked by Schinzel, motivated by a question of Erdős and Selfridge (see 7). The answer is no, as proved by Balister, Bollobás, Morris, Sahasrabudhe, and Tiba [BBMST22].

The moduli of a CoveringSystem ℤ are the ideals \((m_i)\); the modulus \(m_i\) divides \(m_j\) exactly when \((m_j)\subseteq (m_i)\).

theorem erdos_586 :
    ¬ ∃ c : CoveringSystem ℤ, Pairwise fun i j ↦ ¬ c.moduli j ≤ c.moduli i

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/586.lean, line 55.

Sources
LeanErdos586.erdos_586

TheoremErdős Problem 587#

Reference: erdosproblems.com/587

Quoted from FormalConjectures/ErdosProblems/587.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/587.

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

Erdos587.erdos_587.variants.nguyen_vu

Solved: stated here without proof.

Nguyen and Vu proved that \(|A| \ll N^{1/3} (\log N)^{O(1)}\).

theorem erdos_587.variants.nguyen_vu : ∃ᵉ (O > 0) (O' > 0),
    ∀ᶠ N in Filter.atTop, (MaxNotSqSum N : ℝ) ≤ O' * Real.nthRoot 3 N * (N : ℝ).log^O

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/587.lean, line 43.

Sources
LeanErdos587.erdos_587.variants.nguyen_vu

TheoremErdős Problem 588#

References: - erdosproblems.com/588 - [BGS74] Burr, Stefan A. and Grünbaum, Branko and Sloane, N. J. A., The orchard problem. Geometriae Dedicata (1974), 397-424. - [Er84] Erdős, P., Research problems. Period. Math. Hungar. (1984), 101-103. - [FuPa84] Füredi, Z. and Palásti, I., Arrangements of lines with a large number of triangles. Proc. Amer. Math. Soc. (1984), 561-566. - [Gr76] Grünbaum, Branko, New views on some old questions of combinatorial geometry. Colloquio Internazionale sulle Teorie Combinatorie (Roma, 1973), Tomo I (1976), 451-468. - [Ka63] Kárteszi, F., Sylvester egy tételéről és Erdős egy sejtéséről. Matematikai Lapok (1963), 3-10. - [SoSt13] Solymosi, József and Stojaković, Miloš, Many collinear \(k\)-tuples with no \(k+1\) collinear points. Discrete Comput. Geom. (2013), 811-820.

Quoted from FormalConjectures/ErdosProblems/588.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/588.

The file states 9 research or textbook statements: 1 open, 7 solved and 1 textbook result.

Erdos588.erdos_588

Open: stated without proof.

Let \(f_k(n)\) be minimal such that if \(n\) points in \(\mathbb{R}^2\) have no \(k+1\) points on a line then there must be at most \(f_k(n)\) many lines containing at least \(k\) points. Is it true that

\[f_k(n) = o(n^2)\]

for \(k \geq 4\)?

The case \(k = 4\) is Erdős Problem 101. The restriction \(k \geq 4\) is needed: see Erdos588.erdos_588.variants.three_not_isLittleO.

theorem erdos_588 :
    ∀ k : ℕ, 4 ≤ k →
      (fun n : ℕ ↦ (numLinesWithPointsMax k n : ℝ)) =o[atTop] (fun n : ℕ ↦ (n : ℝ) ^ 2)

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

Erdos588.erdos_588.variants.trivial_upper

Textbook result, stated without proof. A Lean proof is at https://github.com/veljjanoski/formal-conjectures-proofs/blob/a199537b29d77124f8e1ea0d816a881e96f0cc0f/FcProofs/Erdos588.lean#L81.

The trivial upper bound, by counting pairs of points: for \(k \geq 2\),

\[f_k(n) \cdot k(k-1) \leq n(n-1).\]
theorem erdos_588.variants.trivial_upper (k n : ℕ) (hk : 2 ≤ k) :
    numLinesWithPointsMax k n * (k * (k - 1)) ≤ n * (n - 1)

Category textbook; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/588.lean, line 77.

Erdos588.erdos_588.variants.sylvester

Solved: stated here without proof.

Sylvester showed (see [BGS74]) that

\[f_3(n) = \frac{n^2}{6} + O(n).\]

The upper bound \(f_3(n) \leq n(n-1)/6\) is Erdos588.erdos_588.variants.trivial_upper with \(k = 3\). The lower bound comes from a construction on a cubic curve.

theorem erdos_588.variants.sylvester :
    (fun n : ℕ ↦ (numLinesWithPointsMax 3 n : ℝ) - (n : ℝ) ^ 2 / 6) =O[atTop]
      (fun n : ℕ ↦ (n : ℝ))

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

Erdos588.erdos_588.variants.three_lower

Solved: stated here without proof.

Burr, Grünbaum, and Sloane [BGS74] and Füredi and Palásti [FuPa84] gave constructions which show that

\[f_3(n) \geq \left(\frac{1}{6} + o(1)\right) n^2.\]
theorem erdos_588.variants.three_lower :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (1 / 6 - ε) * (n : ℝ) ^ 2 ≤ (numLinesWithPointsMax 3 n : ℝ)

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

Erdos588.erdos_588.variants.three_not_isLittleO

Solved: stated here without proof.

The restriction to \(k \geq 4\) in Erdos588.erdos_588 is necessary: \(f_3(n)\) is not \(o(n^2)\). This follows from Erdos588.erdos_588.variants.sylvester.

theorem erdos_588.variants.three_not_isLittleO :
    ¬ (fun n : ℕ ↦ (numLinesWithPointsMax 3 n : ℝ)) =o[atTop] (fun n : ℕ ↦ (n : ℝ) ^ 2)

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

Erdos588.erdos_588.variants.karteszi

Solved: stated here without proof.

Kárteszi [Ka63] proved that for \(k \geq 4\),

\[f_k(n) \gg_k n \log n,\]

resolving a conjecture of Erdős that \(f_k(n)/n \to \infty\).

theorem erdos_588.variants.karteszi :
    ∀ k : ℕ, 4 ≤ k → ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      c * (n : ℝ) * Real.log (n : ℝ) ≤ (numLinesWithPointsMax k n : ℝ)

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

Erdos588.erdos_588.variants.grunbaum

Solved: stated here without proof.

Grünbaum [Gr76] proved that for \(k \geq 4\),

\[f_k(n) \gg_k n^{1 + \frac{1}{k-2}}.\]
theorem erdos_588.variants.grunbaum :
    ∀ k : ℕ, 4 ≤ k → ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      c * (n : ℝ) ^ (1 + 1 / ((k : ℝ) - 2)) ≤ (numLinesWithPointsMax k n : ℝ)

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

Erdos588.erdos_588.variants.solymosi_stojakovic

Solved: stated here without proof.

Solymosi and Stojaković [SoSt13] proved that for \(k \geq 4\),

\[f_k(n) \gg_k n^{2 - O_k(1/\sqrt{\log n})}.\]
theorem erdos_588.variants.solymosi_stojakovic :
    ∀ k : ℕ, 4 ≤ k → ∃ c > (0 : ℝ), ∃ C > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      c * (n : ℝ) ^ (2 - C / Real.sqrt (Real.log (n : ℝ))) ≤
        (numLinesWithPointsMax k n : ℝ)

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

Erdos588.erdos_588.variants.grunbaum_order

Solved: stated here without proof.

Erdős speculated that Grünbaum's bound \(n^{1 + \frac{1}{k-2}}\) may be the correct order of magnitude of \(f_k(n)\) for \(k \geq 4\). This is false: by Erdos588.erdos_588.variants.solymosi_stojakovic [SoSt13], for every \(k \geq 4\) we have \(f_k(n) \neq O(n^{1 + \frac{1}{k-2}})\).

theorem erdos_588.variants.grunbaum_order :
    ∀ k : ℕ, 4 ≤ k →
      ¬ (fun n : ℕ ↦ (numLinesWithPointsMax k n : ℝ)) =O[atTop]
        (fun n : ℕ ↦ (n : ℝ) ^ (1 + 1 / ((k : ℝ) - 2)))

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

Sources
LeanErdos588.erdos_588 · Erdos588.erdos_588.variants.trivial_upper · Erdos588.erdos_588.variants.sylvester · Erdos588.erdos_588.variants.three_lower · Erdos588.erdos_588.variants.three_not_isLittleO · Erdos588.erdos_588.variants.karteszi · Erdos588.erdos_588.variants.grunbaum · Erdos588.erdos_588.variants.solymosi_stojakovic · Erdos588.erdos_588.variants.grunbaum_order

TheoremErdős Problem 590#

References: - erdosproblems.com/590 - [Ch72] Chang, C. C., A partition theorem for the complete graph on {\(\omega\sp{\omega }\)}. J. Combinatorial Theory Ser. A (1972), 396-452. - [Sp57] Specker, Ernst, Teilmengen von Mengen mit Relationen. Comment. Math. Helv. (1957), 302-314. - [La73] Larson, Jean A., A short proof of a partition theorem for the ordinal {\(\omega \sp{\omega }\)}. Ann. Math. Logic (1973/74), 129-145.

Quoted from FormalConjectures/ErdosProblems/590.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/590.

The file states 4 research or textbook statements: 4 solved.

Erdos590.erdos_590

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

Let \(α\) be the infinite ordinal \(\omega^{\omega}\). It was proved by Chang [Ch72] that any red/blue colouring of the edges of \(K_α\) there is either a red \(K_α\) or a blue \(K_3\).

theorem erdos_590 : OrdinalCardinalRamsey (ω ^ ω) (ω ^ ω) 3

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

Erdos590.erdos_590.variants.two

Solved: stated here without proof.

Specker [Sp57] proved that when \(α=ω^2\) any red/blue colouring of the edges of \(K_α\) there is either a red \(K_α\) or a blue \(K_3\).

theorem erdos_590.variants.two : OrdinalCardinalRamsey (ω ^ 2) (ω ^ 2) 3

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

Erdos590.erdos_590.variants.ge_three_false

Solved: stated here without proof.

Specker [Sp57] proved that when \(α=ω^n\) for \(3≤ n < \omega\) then it is not the case that any red/blue colouring of the edges of \(K_α\) there is either a red \(K_α\) or a blue \(K_3\).

theorem erdos_590.variants.ge_three_false {n : ℕ} (h : 3 ≤ n) :
    ¬ OrdinalCardinalRamsey (ω ^ n) (ω ^ n) 3

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

Erdos590.erdos_590.variants.finite_cardinal

Solved: stated here without proof.

Let m be a finite cardinal \(< \omega\). Let \(α\) be the infinite ordinal \(\omega^{\omega}\). It was proved by Milnor that any red/blue colouring of the edges of \(K_α\) there is either a red \(K_α\) or a blue \(K_3\). A shorter proof was found by Larson [La73]

theorem erdos_590.variants.finite_cardinal (m : ℕ) : OrdinalCardinalRamsey (ω ^ ω) (ω ^ ω) m

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

Sources
LeanErdos590.erdos_590 · Erdos590.erdos_590.variants.two · Erdos590.erdos_590.variants.ge_three_false · Erdos590.erdos_590.variants.finite_cardinal

TheoremErdős Problem 591#

References: - erdosproblems.com/591 - [Sc10] Schipperus, Rene, Countable partition ordinals. Ann. Pure Appl. Logic (2010), 1195-1215.

Quoted from FormalConjectures/ErdosProblems/591.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/591.

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

Erdos591.erdos_591

Solved: stated here without proof.

Let \(α\) be the infinite ordinal \(\omega^{\omega^2}\). Is it true that any red/blue colouring of the edges of \(K_α\) there is either a red \(K_α\) or a blue \(K_3\)?

This is true and was proved independently by Schipperus [Sc10] and Darby.

theorem erdos_591 : OrdinalCardinalRamsey (ω ^ ω ^ 2) (ω ^ ω ^ 2) 3

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

Sources
LeanErdos591.erdos_591

TheoremErdős Problem 592#

Reference: erdosproblems.com/592

Quoted from FormalConjectures/ErdosProblems/592.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/592.

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

Erdos592.erdos_592

Open: stated without proof.

Determine which countable ordinals \(β\) have the property that, if \(α = \omega^β\), then in any red/blue colouring of the edges of \(K_α\) there is either a red \(K_α\) or a blue \(K_3\).

theorem erdos_592 (β : Ordinal.{u}) : β.card ≤ ℵ₀ →
    (OrdinalCardinalRamsey (ω ^ β) (ω ^ β) 3 ↔ erdos_592.answer β)

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

Sources
LeanErdos592.erdos_592

TheoremErdős Problem 593#

References: - erdosproblems.com/593 - [EGH75] Erdős, Paul and Galvin, Fred and Hajnal, András, On set-systems having large chromatic number and not containing prescribed subsystems. Infinite and finite sets (Colloq., Keszthely, 1973; dedicated to P. Erdős on his 60th birthday), Vol. I. Colloq. Math. Soc. János Bolyai 10, North-Holland (1975), 425–513. - [Er95d] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) 47 (1992), no. 2, 231–240 (1995). - [EHR73] Erdős, Paul and Hajnal, András and Rothschild, Bruce, On chromatic number of graphs and set-systems. Cambridge Summer School in Mathematical Logic (Cambridge, 1971), Lecture Notes in Math. 337, Springer (1973), 531–538.

Quoted from FormalConjectures/ErdosProblems/593.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/593.

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

Erdos593.erdos_593

Open: stated without proof.

Erdős Problem 593 ($500): Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number \(> \aleph_0\).

The answer is the set of obligatory finite 3-uniform hypergraphs, represented here on the labelled vertex sets Fin n.

Two-colorability (Property B) is a necessary condition, see erdos_593.variants.obligatory_implies_two_colorable, but it is not sufficient: two triples sharing a pair form a 2-colorable hypergraph that is not obligatory, see erdos_593.variants.common_pair_not_obligatory. In the graph case (\(r = 2\)) the problem is completely solved by Erdős–Galvin–Hajnal [EGH75]: the obligatory graphs are exactly the finite bipartite graphs.

A resolution has been claimed by E. Li (arXiv:2606.24882, 2026); at the time of writing erdosproblems.com still lists the problem as open.

theorem erdos_593 :
    {p : Σ n : ℕ, UniformHypergraph (Fin n) 3 | p.2.IsObligatory} = erdos_593.answer

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

Erdos593.erdos_593.variants.obligatory_implies_two_colorable

Solved: stated here without proof.

Necessary direction: every obligatory finite 3-uniform hypergraph is 2-colorable.

This follows from two constructions in [EGH75]. By [EHR73] (see [EGH75, p. 426]) there are 3-uniform hypergraphs of arbitrarily large chromatic number consisting of edge-disjoint triples, so an obligatory F is linear (no two edges share two vertices). By the remark preceding [EGH75, Theorem 10.9] there are, for every infinite cardinal \(\kappa\), 3-uniform hypergraphs of chromatic number \(> \kappa\) all of whose linear sub-hypergraphs are 2-colorable. An obligatory F appears in such a hypergraph, hence is 2-colorable.

theorem erdos_593.variants.obligatory_implies_two_colorable :
    ∀ (W : Type) [Fintype W] (F : UniformHypergraph W 3),
      F.IsObligatory → F.IsNColorable 2

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

Erdos593.erdos_593.variants.two_colorable_implies_obligatory

Solved: stated here without proof.

Sufficient direction fails: it is not the case that every finite 2-colorable 3-uniform hypergraph is obligatory.

The hypergraph commonPair with edges \(\{0,1,2\}\) and \(\{0,1,3\}\) is 2-colorable but does not appear in the 3-uniform hypergraphs of large chromatic number consisting of edge-disjoint triples constructed in [EHR73], see erdos_593.variants.common_pair_not_obligatory.

theorem erdos_593.variants.two_colorable_implies_obligatory :
    ¬ ∀ (W : Type) [Fintype W] (F : UniformHypergraph W 3),
      F.IsNColorable 2 → F.IsObligatory

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

Erdos593.erdos_593.variants.common_pair_not_obligatory

Solved: stated here without proof.

Two triples sharing a pair are not obligatory: by [EHR73] (see [EGH75, p. 426]) there are 3-uniform hypergraphs of arbitrarily large chromatic number consisting of edge-disjoint triples, and commonPair does not appear in any of them.

theorem erdos_593.variants.common_pair_not_obligatory : ¬ commonPair.IsObligatory

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

Erdos593.erdos_593.variants.graph_case_bipartite_obligatory

Solved: stated here without proof.

Graph analogue — bipartite graphs are obligatory (Erdős–Galvin–Hajnal [EGH75]): For the 2-uniform (graph) case, a graph of chromatic cardinal \(> \aleph_0\) must contain all finite bipartite graphs. Specifically, for every finite bipartite graph F and every graph G with chromatic cardinal \(> \aleph_0\), there is a graph embedding from F into G.

This uses F ⊑ G (SimpleGraph.IsContained, an injective graph homomorphism), aligned with the injective edge-preserving map used in the hypergraph Appears definition. A graph embedding F ↪g G would require an induced copy, which the theorem does not provide.

theorem erdos_593.variants.graph_case_bipartite_obligatory :
    ∀ (V : Type*) (G : SimpleGraph V),
      ℵ₀ < G.chromaticCardinal →
      ∀ (W : Type*) [Fintype W] (F : SimpleGraph W), F.IsBipartite →
        F ⊑ G

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

Erdos593.erdos_593.variants.graph_case_no_odd_cycle

Solved: stated here without proof.

Graph analogue — no odd cycle is obligatory (Erdős–Galvin–Hajnal [EGH75]): For every odd \(k \geq 3\), there exists a graph with chromatic cardinal \(\aleph_1\) that contains no cycle of length \(k\). This shows the class of obligatory graphs is strictly smaller than all finite graphs.

theorem erdos_593.variants.graph_case_no_odd_cycle :
    ∀ k : ℕ, Odd k → 3 ≤ k →
      ∃ (V : Type*) (G : SimpleGraph V),
        G.chromaticCardinal = ℵ_ 1 ∧
        IsEmpty (cycleGraph k →g G)

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

Erdos593.erdos_593.variants.uncountable_vertices_if_large_chromatic

Textbook result, proved here.

Vertices must be uncountable: Every 3-uniform hypergraph with chromatic cardinal \(> \aleph_0\) must have an uncountable vertex set.

Proof: If V is countable, there exists an injection φ : V → ℕ. Using distinct natural numbers as colors gives a proper coloring, so \(\chi(H) \leq \#\mathbb{N} = \aleph_0\), contradicting \(\chi(H) > \aleph_0\).

theorem erdos_593.variants.uncountable_vertices_if_large_chromatic
    {V : Type} (H : UniformHypergraph V 3) (hχ : ℵ₀ < H.chromaticCardinal) :
    ¬ Countable V

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/593.lean, line 166.

Erdos593.erdos_593.variants.nonempty_edges_if_large_chromatic

Textbook result, proved here.

No hyperedges implies chromatic cardinal ≤ 1: A 3-uniform hypergraph with no edges can be properly colored with a single color, so its chromatic cardinal is at most 1. In particular, \(\chi(H) > \aleph_0\) implies H has at least one hyperedge.

theorem erdos_593.variants.nonempty_edges_if_large_chromatic
    {V : Type} (H : UniformHypergraph V 3) (hχ : ℵ₀ < H.chromaticCardinal) :
    H.edgeSet.Nonempty

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/593.lean, line 183.

Erdos593.erdos_593.variants.obligatory_monotone

Textbook result, proved here.

Monotonicity of the obligatory property: If F₁ appears in F₂ and F₂ is obligatory, then F₁ is also obligatory.

Proof: For any H with \(\chi(H) > \aleph_0\), since F₂ is obligatory, F₂ appears in H via some injection φ₂. Since F₁ appears in F₂ via φ₁, the composition φ₂ ∘ φ₁ witnesses that F₁ appears in H.

theorem erdos_593.variants.obligatory_monotone
    {W₁ W₂ : Type} [Fintype W₁] [Fintype W₂] [DecidableEq W₂]
    {F₁ : UniformHypergraph W₁ 3} {F₂ : UniformHypergraph W₂ 3}
    (h12 : F₁.Appears F₂) (hObl : F₂.IsObligatory) :
    F₁.IsObligatory

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/593.lean, line 207.

Erdos593.erdos_593.variants.empty_hypergraph_obligatory

Textbook result, proved here.

The empty hypergraph is trivially obligatory: The 3-uniform hypergraph on PEmpty (no vertices, no edges) appears in every hypergraph via the empty injection.

This degenerate case confirms the definition is well-formed.

theorem erdos_593.variants.empty_hypergraph_obligatory :
    UniformHypergraph.IsObligatory (W := PEmpty) (k := 3)
      (UniformHypergraph.ofFinset ∅ (by simp [Finset.IsUniform]))

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/593.lean, line 222.

Sources
LeanErdos593.erdos_593 · Erdos593.erdos_593.variants.obligatory_implies_two_colorable · Erdos593.erdos_593.variants.two_colorable_implies_obligatory · Erdos593.erdos_593.variants.common_pair_not_obligatory · Erdos593.erdos_593.variants.graph_case_bipartite_obligatory · Erdos593.erdos_593.variants.graph_case_no_odd_cycle · Erdos593.erdos_593.variants.uncountable_vertices_if_large_chromatic · Erdos593.erdos_593.variants.nonempty_edges_if_large_chromatic · Erdos593.erdos_593.variants.obligatory_monotone · Erdos593.erdos_593.variants.empty_hypergraph_obligatory

TheoremErdős Problem 594#

References: - erdosproblems.com/594 - [ErHa66] Erdős, P. and Hajnal, A., On chromatic number of graphs and set-systems. Acta Math. Acad. Sci. Hungar. (1966), 61-99. - [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. - [EHS74] Erdős, P. and Hajnal, A. and Shelah, S., On some general properties of chromatic numbers. Topics in topology (Proc. Colloq., Keszthely, 1972) (1974), 243-255.

Quoted from FormalConjectures/ErdosProblems/594.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/594.

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

Erdos594.erdos_594

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

Erdős Problem 594 (Erdős–Hajnal [ErHa66], [Er69b]):

Does every graph \(G\) with chromatic number \(\geq \aleph_1\) contain all sufficiently large odd cycles?

The answer is Yes, proved by Erdős, Hajnal, and Shelah [EHS74].

A graph has chromatic number \(\geq \aleph_1\) (i.e. uncountable chromatic number) if and only if it admits no proper colouring with countably many colours; this is encoded as IsEmpty (G.Coloring ℕ). The conclusion states that there is some \(N\) such that for every \(k \geq N\) the graph contains a cycle of odd length \(2k + 1\).

theorem erdos_594 :
    ∀ (V : Type) (G : SimpleGraph V), IsEmpty (G.Coloring ℕ) →
      ∃ N : ℕ, ∀ k : ℕ, N ≤ k →
        ∃ (v : V) (w : G.Walk v v), w.IsCycle ∧ w.length = 2 * k + 1

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

Erdos594.erdos_594.variants.erdos_hajnal

Solved: stated here without proof.

The earlier result of Erdős and Hajnal [ErHa66]: every graph with chromatic number \(\geq \aleph_2\) contains all sufficiently large odd cycles.

Chromatic number \(\geq \aleph_2\) is encoded as the nonexistence of a proper colouring with any set of at most \(\aleph_1\) colours.

theorem erdos_594.variants.erdos_hajnal (V : Type) (G : SimpleGraph V)
    (h : ∀ (α : Type), #α ≤ ℵ_ 1 → IsEmpty (G.Coloring α)) :
    ∃ N : ℕ, ∀ k : ℕ, N ≤ k →
      ∃ (v : V) (w : G.Walk v v), w.IsCycle ∧ w.length = 2 * k + 1

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

Sources
LeanErdos594.erdos_594 · Erdos594.erdos_594.variants.erdos_hajnal

TheoremErdős Problem 595#

References: - erdosproblems.com/595 - [Er87] Erdős, Paul, Problems and results on set systems and hypergraphs. Extremal problems for finite sets (Visegrád, 1991), Bolyai Soc. Math. Stud. (1994), 217-227. - [Fo70] Folkman, Jon, Graphs with monochromatic complete subgraphs in every edge coloring. SIAM J. Appl. Math. (1970), 19:340-345. - [NeRo75] Nešetřil, Jaroslav and Rödl, Vojtěch, Type theory of partition problems of graphs. Recent advances in graph theory (Proc. Second Czechoslovak Sympos., Prague, 1974), Academia, Prague (1975), 405-412.

Quoted from FormalConjectures/ErdosProblems/595.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/595.

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

Erdos595.erdos_595

Open: stated without proof.

Erdős Problem 595 ($250): Is there an infinite graph \(G\) which contains no \(K_4\) and is not the union of countably many triangle-free graphs?

A problem of Erdős and Hajnal [Er87].

theorem erdos_595 :
    ∃ (V : Type*) (_ : Infinite V) (G : SimpleGraph V),
      G.CliqueFree 4 ∧ ¬IsCountableUnionOfTriangleFree G

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

Erdos595.erdos_595.variants.folkman_finite

Solved: stated here without proof.

Folkman–Nešetřil–Rödl (finite version) [Fo70, NeRo75]: For every n ≥ 1, there exists a graph G (on a finite vertex set) that contains no \(K_4\) and whose edges cannot be covered by n triangle-free graphs.

More precisely: for every n : ℕ with 1 ≤ n, there exist a finite type V and a graph G : SimpleGraph V with: 1. G.CliqueFree 4 (no \(K_4\)), and 2. For every family H : Fin n → SimpleGraph V of triangle-free graphs, G ≠ ⨆ i, H i.

This is the finite analogue of Problem 595. The proofs of Folkman [Fo70] and Nešetřil–Rödl [NeRo75] give different explicit constructions.

theorem erdos_595.variants.folkman_finite :
    ∀ n : ℕ, 1 ≤ n →
    ∃ (V : Type*) (_ : Fintype V) (G : SimpleGraph V),
      G.CliqueFree 4 ∧
      ∀ (H : Fin n → SimpleGraph V), (∀ i, (H i).CliqueFree 3) → G ≠ ⨆ i, H i

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

Erdos595.erdos_595.variants.subgraph_of_countable_union

Textbook result, proved here.

Monotonicity: If G is a countable union of triangle-free graphs and H ≤ G (i.e., H is a subgraph of G), then H is also a countable union of triangle-free graphs.

Proof: If G = ⨆ i, G_i with each G_i triangle-free, then H = ⨆ i, H ⊓ G_i. Each H ⊓ G_i is triangle-free because it is a subgraph of G_i.

theorem erdos_595.variants.subgraph_of_countable_union
    {V : Type*} {G H : SimpleGraph V}
    (hH : H ≤ G) (hG : IsCountableUnionOfTriangleFree G) :
    IsCountableUnionOfTriangleFree H

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/595.lean, line 93.

Erdos595.erdos_595.variants.triangle_free_is_union

Textbook result, proved here.

Triangle-free graphs are trivially countable unions of triangle-free graphs: if G is already triangle-free, then G = ⨆ i : ℕ, G_i where G_0 = G and G_i = ⊥ for i ≥ 1.

theorem erdos_595.variants.triangle_free_is_union
    {V : Type*} (G : SimpleGraph V) (hG : G.CliqueFree 3) :
    IsCountableUnionOfTriangleFree G

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/595.lean, line 115.

Erdos595.erdos_595.variants.complete_nat_is_union

Textbook result, proved here.

The complete graph ⊤ on ℕ is a countable union of triangle-free graphs: we decompose it into the family of star graphs {H_m}_{m : ℕ}, where H_m is the graph with edges {m, n} for all n ≠ m. Each star is triangle-free (any two non-center vertices share no edge within the star), and their union covers all edges of ⊤.

Proof sketch (star triangle-free): If {a, b, c} were a triangle in H_m, then each of the three edges {a, b}, {a, c}, {b, c} would pass through m. In particular, from {a, b} we get a = m or b = m; from {b, c} we get b = m or c = m. Case analysis shows that two vertices must equal m, contradicting the triangle having three distinct vertices.

theorem erdos_595.variants.complete_nat_is_union :
    IsCountableUnionOfTriangleFree (⊤ : SimpleGraph ℕ)

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/595.lean, line 144.

Erdos595.erdos_595.variants.K4_not_cliqueFree

Textbook result, proved here.

The complete graph ⊤ on Fin 4 is not \(K_4\)-free: ⊤ on Fin 4 equals the complete graph \(K_4\), so it contains \(K_4\) as a subgraph and is not \(K_4\)-free.

This sanity check confirms the \(K_4\)-free hypothesis of Problem 595 is non-trivial.

theorem erdos_595.variants.K4_not_cliqueFree :
    ¬ (⊤ : SimpleGraph (Fin 4)).CliqueFree 4

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/595.lean, line 198.

Sources
LeanErdos595.erdos_595 · Erdos595.erdos_595.variants.folkman_finite · Erdos595.erdos_595.variants.subgraph_of_countable_union · Erdos595.erdos_595.variants.triangle_free_is_union · Erdos595.erdos_595.variants.complete_nat_is_union · Erdos595.erdos_595.variants.K4_not_cliqueFree

TheoremErdős Problem 596#

References: - erdosproblems.com/596 - [Er87] Erdős, Some of my favourite problems in various branches of combinatorics, Mat. Lapok 1987. - [NeRo75] Nešetřil and Rödl, The Ramsey property for graphs with forbidden complete subgraphs, J. Combin. Theory B 20 (1976), 243--249.

Quoted from FormalConjectures/ErdosProblems/596.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/596.

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

Erdos596.erdos_596

Open: stated without proof.

Erdős Problem 596 (Erdős–Hajnal, [Er87]). For which graph pairs \((G_1, G_2)\) is it true that

(1) for every \(n \geq 1\) there is a graph \(H\) without a \(G_1\) such that any \(n\)-colouring of \(H\)'s edges contains a monochromatic \(G_2\), and yet (2) for every graph \(H\) without a \(G_1\) there is an \(\aleph_0\)-colouring of \(H\)'s edges with no monochromatic \(G_2\)?

Erdős and Hajnal originally conjectured that no such pair exists; but \((C_4, C_6)\) witnesses it (Nešetřil–Rödl + Erdős–Hajnal). The full question is to characterise the class of all such pairs, recorded here as the unknown erdos_596.answer.

See Problem 595 for the specific case \((G_1, G_2) = (K_4, K_3)\).

theorem erdos_596 :
    ∀ {U₁ U₂ : Type} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂),
      IsErdosHajnalExceptional G₁ G₂ ↔ erdos_596.answer G₁ G₂

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

Erdos596.erdos_596.variants.exists_exceptional

Solved: stated here without proof.

Erdős–Hajnal exceptional pairs exist — recorded as a known direction of erdos_596.

theorem erdos_596.variants.exists_exceptional :
    ∃ (U₁ U₂ : Type) (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂),
      IsErdosHajnalExceptional G₁ G₂

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

Erdos596.erdos_596.variants.C4_free_countable_escape

Solved: stated here without proof.

Every \(C_4\)-free graph is a countable union of trees (Erdős–Hajnal [Er87]); trees are acyclic, hence \(C_6\)-free, giving the countable Ramsey escape for \((C_4, C_6)\).

theorem erdos_596.variants.C4_free_countable_escape :
    HasCountableRamseyEscape (cycleGraph 4) (cycleGraph 6)

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

Erdos596.erdos_596.variants.C4_C6_finite_ramsey

Solved: stated here without proof.

Nešetřil–Rödl [NeRo75]: for every \(n \geq 1\) there is a \(C_4\)-free graph whose edges cannot be \(n\)-coloured without a monochromatic \(C_6\).

theorem erdos_596.variants.C4_C6_finite_ramsey :
    HasFiniteRamseyProperty (cycleGraph 4) (cycleGraph 6)

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

Erdos596.erdos_596.variants.C4_C6_is_exceptional

Proved here.

The pair \((C_4, C_6)\) is Erdős–Hajnal exceptional; combines C4_C6_finite_ramsey and C4_free_countable_escape.

theorem erdos_596.variants.C4_C6_is_exceptional :
    IsErdosHajnalExceptional (cycleGraph 4) (cycleGraph 6)

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

Erdos596.erdos_596.variants.original_conjecture_is_false

Solved: stated here without proof.

The original Erdős–Hajnal conjecture (that no exceptional pair exists) is false — witnessed by \((C_4, C_6)\) via C4_C6_is_exceptional.

theorem erdos_596.variants.original_conjecture_is_false :
    ¬ ∀ {U₁ U₂ : Type} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂),
      ¬IsErdosHajnalExceptional G₁ G₂

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

Erdos596.erdos_596.variants.K4_K3_exceptional_iff

Open: stated without proof.

Whether \((K_4, K_3)\) is Erdős–Hajnal exceptional is precisely the content of Erdős Problem 595. The finite Ramsey property holds (Folkman 1970, Nešetřil–Rödl [NeRo75]); the open part is whether every \(K_4\)-free graph is a countable union of triangle-free graphs.

theorem erdos_596.variants.K4_K3_exceptional_iff :
    IsErdosHajnalExceptional (completeGraph (Fin 4)) (completeGraph (Fin 3))

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

Erdos596.erdos_596.variants.K4_K3_finite_ramsey

Solved: stated here without proof.

Folkman 1970 / Nešetřil–Rödl [NeRo75]: for every \(n \geq 1\) there is a \(K_4\)-free graph whose edges cannot be \(n\)-coloured without a monochromatic triangle.

theorem erdos_596.variants.K4_K3_finite_ramsey :
    HasFiniteRamseyProperty (completeGraph (Fin 4)) (completeGraph (Fin 3))

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

Sources
LeanErdos596.erdos_596 · Erdos596.erdos_596.variants.exists_exceptional · Erdos596.erdos_596.variants.C4_free_countable_escape · Erdos596.erdos_596.variants.C4_C6_finite_ramsey · Erdos596.erdos_596.variants.C4_C6_is_exceptional · Erdos596.erdos_596.variants.original_conjecture_is_false · Erdos596.erdos_596.variants.K4_K3_exceptional_iff · Erdos596.erdos_596.variants.K4_K3_finite_ramsey

TheoremErdős Problem 597#

Reference: erdosproblems.com/597

References: - [Er87] Erdős, P., Some problems on finite and infinite graphs. Logic and combinatorics (Arcata, Calif., 1985) (1987), 223-228.

Quoted from FormalConjectures/ErdosProblems/597.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/597.

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

Erdos597.erdos_597

Open: stated without proof.

Erdős Problem 597 [Er87]. Let \(G\) be a graph on at most \(\aleph_1\) vertices which contains no \(K_4\) and no \(K_{\aleph_0,\aleph_0}\) (the complete bipartite graph with \(\aleph_0\) vertices in each class). Is it true that

\[\omega_1^2 \to (\omega_1 \omega, G)^2?\]
theorem erdos_597 :
    ∀ (W : Type) (G : SimpleGraph W), #W ≤ ℵ_ 1 → G.CliqueFree 4 →
      (¬ ∃ A B : Set W, Disjoint A B ∧ A.Infinite ∧ B.Infinite ∧
        ∀ a ∈ A, ∀ b ∈ B, G.Adj a b) →
      OrdinalGraphRamsey ((ω_ 1) ^ (2 : ℕ)) ((ω_ 1) * ω) G

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

Erdos597.erdos_597.variants.finite

Open: stated without proof.

Erdős Problem 597, finite case [Er87]. Is it true that \(\omega_1^2 \to (\omega_1 \omega, G)^2\) for every finite \(K_4\)-free graph \(G\)? (A finite graph contains no \(K_{\aleph_0,\aleph_0}\), so that hypothesis is vacuous.)

theorem erdos_597.variants.finite :
    ∀ (W : Type) [Fintype W] (G : SimpleGraph W), G.CliqueFree 4 →
      OrdinalGraphRamsey ((ω_ 1) ^ (2 : ℕ)) ((ω_ 1) * ω) G

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

Erdos597.erdos_597.variants.erdos_hajnal

Solved: stated here without proof.

Erdős and Hajnal proved that \(\omega_1^2 \to (\omega_1 \omega, 3)^2\): in every red/blue colouring of the edges of the complete graph on \(\omega_1^2\) there is either a red clique of order type \(\omega_1 \cdot \omega\) or a blue triangle.

theorem erdos_597.variants.erdos_hajnal :
    OrdinalCardinalRamsey ((ω_ 1) ^ (2 : ℕ)) ((ω_ 1) * ω) 3

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

Erdos597.erdos_597.variants.baumgartner

Solved: stated here without proof.

Erdős originally asked Problem 597 with just the assumption that \(G\) is \(K_4\)-free, but Baumgartner proved that \(\omega_1^2 \not\to (\omega_1 \omega, K_{\aleph_0,\aleph_0})^2\).

theorem erdos_597.variants.baumgartner :
    ¬ OrdinalGraphRamsey ((ω_ 1) ^ (2 : ℕ)) ((ω_ 1) * ω) (completeBipartiteGraph ℕ ℕ)

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

Sources
LeanErdos597.erdos_597 · Erdos597.erdos_597.variants.finite · Erdos597.erdos_597.variants.erdos_hajnal · Erdos597.erdos_597.variants.baumgartner

TheoremErdős Problem 598#

Reference: erdosproblems.com/598

Quoted from FormalConjectures/ErdosProblems/598.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/598.

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

Erdos598.erdos_598

Open: stated without proof.

Erdős Problem 598: Let \(m\) be an infinite cardinal and \(\kappa\) be the successor cardinal of \(2^{\aleph_0}\). Can one colour the countable subsets of \(m\) using \(\kappa\) many colours so that every \(X \subseteq m\) with \(|X| = \kappa\) contains subsets of all possible colours?

theorem erdos_598 :
    ∀ (m : Type*) [Infinite m],
    ∃ c : { s : Set m // s.Countable } → κ.out,
    ∀ X : Set m, #X = κ →
    c '' { s : { sub : Set m // sub.Countable } | s.1 ⊆ X } = Set.univ

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

Sources
LeanErdos598.erdos_598

TheoremErdős Problem 599#

References: - erdosproblems.com/599 - [AhBe09] Aharoni, Ron and Berger, Eli, Menger's theorem for infinite graphs, Invent. Math. 176 (2009), 1--62.

Quoted from FormalConjectures/ErdosProblems/599.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/599.

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

Erdos599.erdos_599

Solved: stated here without proof.

Erdős Problem 599 (the Erdős–Menger conjecture).

Let \(G\) be a (possibly infinite) graph and let \(A, B\) be disjoint independent sets of vertices. Must there exist a family \(P\) of pairwise vertex-disjoint paths from \(A\) to \(B\), and a set \(S\) of vertices containing exactly one vertex from each path in \(P\), such that every path from \(A\) to \(B\) contains at least one vertex of \(S\)?

For finite \(G\) this is equivalent to Menger's theorem. The answer is yes, proved by Aharoni and Berger [AhBe09].

theorem erdos_599 :
    ∀ (V : Type) (G : SimpleGraph V) (A B : Set V),
      Disjoint A B → G.IsIndepSet A → G.IsIndepSet B →
      ∃ (ι : Type) (a b : ι → V) (p : ∀ i, G.Walk (a i) (b i)) (S : Set V),
        (∀ i, a i ∈ A) ∧ (∀ i, b i ∈ B) ∧ (∀ i, (p i).IsPath) ∧
        (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧
        S ⊆ {v | ∃ i, v ∈ (p i).support} ∧
        (∀ i, ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧
        (∀ a' ∈ A, ∀ b' ∈ B, ∀ q : G.Walk a' b', q.IsPath → ∃ v ∈ q.support, v ∈ S)

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

Erdos599.erdos_599.variants.aharoni_berger

Solved: stated here without proof.

Menger's theorem for infinite graphs (Aharoni–Berger [AhBe09]).

The theorem actually proved by Aharoni and Berger holds for arbitrary vertex sets \(A\) and \(B\): in any (possibly infinite) graph \(G\) there is a family \(P\) of pairwise vertex-disjoint \(A\)--\(B\) paths together with an \(A\)--\(B\) separator \(S\) consisting of the choice of exactly one vertex from each path in \(P\). The disjointness and independence hypotheses of erdos_599 are not needed.

theorem erdos_599.variants.aharoni_berger :
    ∀ (V : Type) (G : SimpleGraph V) (A B : Set V),
      ∃ (ι : Type) (a b : ι → V) (p : ∀ i, G.Walk (a i) (b i)) (S : Set V),
        (∀ i, a i ∈ A) ∧ (∀ i, b i ∈ B) ∧ (∀ i, (p i).IsPath) ∧
        (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧
        S ⊆ {v | ∃ i, v ∈ (p i).support} ∧
        (∀ i, ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧
        (∀ a' ∈ A, ∀ b' ∈ B, ∀ q : G.Walk a' b', q.IsPath → ∃ v ∈ q.support, v ∈ S)

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

Sources
LeanErdos599.erdos_599 · Erdos599.erdos_599.variants.aharoni_berger

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.