Erdős Problem 554 to Erdős Problem 578
TheoremErdős Problem 554#
References: - erdosproblems.com/554 - [Er81c] Erdős, P., Some new problems and results in graph theory and other branches of combinatorial mathematics. Combinatorics and graph theory (Calcutta, 1980), Lecture Notes in Math. 885 (1981), 9-17. - [BoEr73] Bondy, J. A. and Erdős, P., Ramsey numbers for cycles in graphs. J. Combin. Theory Ser. B 14 (1973), 46-54. - [ErGr75] Erdős, P. and Graham, R. L., On partition theorems for finite graphs. Infinite and finite sets (Colloq., Keszthely, 1973), Colloq. Math. Soc. János Bolyai 10 (1975), 515-527. - [DaJo17] Day, A. N. and Johnson, J. R., Multicolour Ramsey numbers of odd cycles. J. Combin. Theory Ser. B 124 (2017), 56-63. arXiv:1602.07607 - [JeSk21] Jenssen, M. and Skokan, J., Exact Ramsey numbers of odd cycles via nonlinear optimisation. Adv. Math. 376 (2021), Paper No. 107444. arXiv:1608.05705 - [ACJMR26] Axenovich, M., Cames van Batenburg, W., Janzer, O., Michel, L. and Rundström, M., An improved upper bound for the multicolour Ramsey number of odd cycles. J. Combin. Theory Ser. B 179 (2026), 293-298. arXiv:2510.17981 doi:10.1016/j.jctb.2026.04.005
Quoted from FormalConjectures/ErdosProblems/554.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/554.
The file states 7 research or textbook statements: 2 open and 5 solved. It also has 3 test statements, counted here but not shown.
Erdos554.erdos_554
Open: stated without proof.
Let \(R_k(G)\) denote the minimal \(m\) such that if the edges of \(K_m\) are \(k\)-coloured then there is a monochromatic copy of \(G\). Show that
\[\lim_{k\to \infty}\frac{R_k(C_{2n+1})}{R_k(K_3)}=0\]for any \(n\geq 2\).
A problem of Erdős and Graham. The case \(n = 1\) is excluded since \(C_3 = K_3\). This problem is
23 in Ramsey Theory in the graphs problem collection.
23 in Ramsey Theory in the graphs problem collection.
theorem erdos_554 (n : ℕ) (hn : 2 ≤ n) :
Tendsto (fun k : ℕ ↦ (multicolourGraphRamsey k (cycleGraph (2 * n + 1)) : ℝ) /
(multicolourGraphRamsey k (completeGraph (Fin 3)) : ℝ)) atTop (𝓝 0)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/554.lean, line 84.
Erdos554.erdos_554.variants.n_eq_two
Open: stated without proof.
The problem is open even for \(n = 2\):
\[\lim_{k\to \infty}\frac{R_k(C_5)}{R_k(K_3)}=0.\]
theorem erdos_554.variants.n_eq_two :
Tendsto (fun k : ℕ ↦ (multicolourGraphRamsey k (cycleGraph 5) : ℝ) /
(multicolourGraphRamsey k (completeGraph (Fin 3)) : ℝ)) atTop (𝓝 0)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/554.lean, line 94.
Erdos554.erdos_554.variants.lower_bound
Solved: stated here without proof.
Bondy and Erdős [BoEr73] and Erdős and Graham [ErGr75] proved the lower bound
\[n2^k+1\leq R_k(C_{2n+1})\]for all \(n, k \geq 1\). The condition \(k \geq 1\) excludes the junk value \(R_0(G) = 2\).
theorem erdos_554.variants.lower_bound :
∀ n : ℕ, 1 ≤ n → ∀ k : ℕ, 1 ≤ k →
n * 2 ^ k + 1 ≤ multicolourGraphRamsey k (cycleGraph (2 * n + 1))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/554.lean, line 105.
Erdos554.erdos_554.variants.upper_bound
Solved: stated here without proof.
Erdős and Graham [ErGr75] (see also [BoEr73]) proved the upper bound
\[R_k(C_{2n+1})\leq 2n(k+2)!\]for all \(n, k \geq 1\).
theorem erdos_554.variants.upper_bound :
∀ n : ℕ, 1 ≤ n → ∀ k : ℕ, 1 ≤ k →
multicolourGraphRamsey k (cycleGraph (2 * n + 1)) ≤ 2 * n * (k + 2).factorial
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/554.lean, line 116.
Erdos554.erdos_554.variants.acjmr
Solved: stated here without proof.
Axenovich, Cames van Batenburg, Janzer, Michel and Rundström [ACJMR26, Theorem 1.1] proved that
\[R_k(C_{2n+1}) \leq (4n-2)^k k^{k/n}+1\]for all \(n, k \geq 1\). For \(n \geq 2\) this improves the upper bound in
Erdos554.erdos_554.variants.upper_bound, since \(k^{k/n}\) grows much more slowly than \((k+2)!\).
theorem erdos_554.variants.acjmr :
∀ n : ℕ, 1 ≤ n → ∀ k : ℕ, 1 ≤ k →
(multicolourGraphRamsey k (cycleGraph (2 * n + 1)) : ℝ) ≤
(4 * n - 2 : ℝ) ^ k * (k : ℝ) ^ ((k : ℝ) / n) + 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/554.lean, line 128.
Erdos554.erdos_554.variants.day_johnson
Solved: stated here without proof.
Day and Johnson [DaJo17] proved that for every \(n \geq 1\) there is a constant \(c_n > 0\) such that
\[R_k(C_{2n+1}) > 2n(2+c_n)^{k-1}\]for all sufficiently large \(k\). So the lower bound in
Erdos554.erdos_554.variants.lower_boundis not sharp for fixed \(n\) and large \(k\).
theorem erdos_554.variants.day_johnson :
∀ n : ℕ, 1 ≤ n → ∃ c > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
(2 * n : ℝ) * (2 + c) ^ (k - 1) <
(multicolourGraphRamsey k (cycleGraph (2 * n + 1)) : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/554.lean, line 141.
Erdos554.erdos_554.variants.jenssen_skokan
Solved: stated here without proof.
Jenssen and Skokan [JeSk21] proved that the lower bound in
Erdos554.erdos_554.variants.lower_boundis sharp for fixed \(k\) and large \(n\): for every \(k \geq 2\),\[R_k(C_{2n+1}) = n2^k+1\]for all sufficiently large \(n\).
theorem erdos_554.variants.jenssen_skokan :
∀ k : ℕ, 2 ≤ k → ∀ᶠ n : ℕ in atTop,
multicolourGraphRamsey k (cycleGraph (2 * n + 1)) = n * 2 ^ k + 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/554.lean, line 155.
Sources
TheoremErdős Problem 555#
Reference: erdosproblems.com/555
Quoted from FormalConjectures/ErdosProblems/555.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/555.
The file states 1 research or textbook statement: 1 open.
Erdos555.erdos_555
Open: stated without proof.
Let \(R_k(G)\) be the least \(m\) such that every \(k\)-colouring of the edges of \(K_m\) contains a monochromatic copy of \(G\). Determine \(R_k(C_{2n})\).
theorem erdos_555 : EvenCycleRamseyFunction erdos_555.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/555.lean, line 67.
Sources
TheoremErdős Problem 556#
A problem of Bondy and Erdős: for the cycle \(C_n\) with \(n \ge 4\), the \(3\)-colour Ramsey number satisfies
\[R(C_n; 3) \le 4n - 3.\]The triangle is excluded: \(C_3 = K_3\) and \(R(K_3; 3) = 17 > 9\) [Rad]. The bound is best possible for odd \(n\), where equality is conjectured (and known for large odd \(n\)). Łuczak proved the asymptotic bound \(R(C_n; 3) \le (4 + o(1))n\), and \((3 + o(1))n\) for even \(n\); Kohayakawa, Simonovits and Skokan settled large odd \(n\), and Benevides and Skokan large even \(n\), but the inequality for all \(n\) remains open.
References: - erdosproblems.com/556 - [Er81] P. Erdős, On the combinatorial problems which I would most like to see solved, Combinatorica 1 (1981), 25-42. - [Lu99] T. Łuczak, \(R(C_n, C_n, C_n) \le (4 + o(1))n\), J. Combin. Theory Ser. B 75 (1999), 174-187. - [KSS05] Y. Kohayakawa, M. Simonovits, J. Skokan, The 3-colored Ramsey number of odd cycles, Proceedings of GRACO2005 (2005), 397-402. - [BeSk09] F. S. Benevides, J. Skokan, The 3-colored Ramsey number of even cycles, J. Combin. Theory Ser. B 99 (2009), 690-708. - [Rad] S. P. Radziszowski, Small Ramsey Numbers, Electron. J. Combin. Dynamic Survey DS1, revision 18, p. 61.
Quoted from FormalConjectures/ErdosProblems/556.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/556.
The file states 6 research or textbook statements: 1 open and 5 solved.
Erdos556.erdos_556
Open: stated without proof.
Erdős Problem 556 (Bondy–Erdős): for all \(n \ge 4\),
\[R(C_n; 3) \le 4n - 3.\]The case \(n = 3\) is excluded since \(R(K_3; 3) = 17\).
theorem erdos_556 (n : ℕ) (hn : 4 ≤ n) :
multicolourRamsey (cycleGraph n) 3 ≤ 4 * n - 3
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/556.lean, line 60.
Erdos556.erdos_556.variants.luczak_asymptotic
Solved: stated here without proof.
Łuczak's asymptotic bound [Lu99]: for every \(\varepsilon > 0\), for all sufficiently large \(n\),
\[R(C_n; 3) \le (4 + \varepsilon)n.\]
theorem erdos_556.variants.luczak_asymptotic :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
(multicolourRamsey (cycleGraph n) 3 : ℝ) ≤ (4 + ε) * n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/556.lean, line 69.
Erdos556.erdos_556.variants.luczak_asymptotic_even
Solved: stated here without proof.
Łuczak's asymptotic bound for even \(n\) [Lu99]: for every \(\varepsilon > 0\), for all sufficiently large even \(n\),
\[R(C_n; 3) \le (3 + \varepsilon)n.\]
theorem erdos_556.variants.luczak_asymptotic_even :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, Even n →
(multicolourRamsey (cycleGraph n) 3 : ℝ) ≤ (3 + ε) * n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/556.lean, line 80.
Erdos556.erdos_556.variants.odd_lower_bound
Solved: stated here without proof.
For odd \(n\) the bound \(4n - 3\) is best possible: the \(3\)-colour Ramsey number is at least \(4n - 3\), so equality holds whenever the conjectured upper bound does.
theorem erdos_556.variants.odd_lower_bound (n : ℕ) (hn : 3 ≤ n) (hodd : Odd n) :
4 * n - 3 ≤ multicolourRamsey (cycleGraph n) 3
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/556.lean, line 90.
Erdos556.erdos_556.variants.kss_large_odd
Solved: stated here without proof.
Kohayakawa, Simonovits and Skokan [KSS05] settled the conjecture for large odd \(n\): for all sufficiently large odd \(n\),
\[R(C_n; 3) = 4n - 3.\]
theorem erdos_556.variants.kss_large_odd :
∀ᶠ n : ℕ in atTop, Odd n → multicolourRamsey (cycleGraph n) 3 = 4 * n - 3
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/556.lean, line 100.
Erdos556.erdos_556.variants.benevides_skokan_large_even
Solved: stated here without proof.
Benevides and Skokan [BeSk09] settled the even case for large \(n\): for all sufficiently large even \(n\),
\[R(C_n; 3) = 2n.\]
theorem erdos_556.variants.benevides_skokan_large_even :
∀ᶠ n : ℕ in atTop, Even n → multicolourRamsey (cycleGraph n) 3 = 2 * n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/556.lean, line 110.
Sources
TheoremErdős Problem 557#
References: - erdosproblems.com/557 - [ErGr75] Erdős, P. and Graham, R. L., On partition theorems for finite graphs. Infinite and finite sets (Colloq., Keszthely, 1973), Vol. I, Colloq. Math. Soc. János Bolyai 10 (1975), 515-527. - [ReSt26] Reed, Bruce and Stein, Maya, The Erdős-Sós conjecture in dense graphs. arXiv:2609.05417 (2026).
Quoted from FormalConjectures/ErdosProblems/557.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/557.
The file states 4 research or textbook statements: 4 solved.
Erdos557.erdos_557
Solved: stated here; a Lean proof is at https://github.com/zhangjun725/erdos557/blob/c4e0ab13027f8bb50defade11cf8a53c7b8b0ba9/Erdos557/Basic.lean#L153.
Let \(R_k(G)\) denote the minimal \(m\) such that if the edges of \(K_m\) are \(k\)-coloured then there is a monochromatic copy of \(G\). Is it true that
\[R_k(T)\leq kn+O(1)\]for any tree \(T\) on \(n\) vertices?
The answer is yes, with an absolute constant: \(R_k(T) \leq kn + 3\) for all \(k\) and \(n\). For \(n \geq 2\) this follows from the explicit bound \(R_k(T) \leq k(n-2)+3\), a consequence of the Erdős–Sós theorem (Erdős problem 548) by the pigeonhole principle, as recorded on the problem page; Reed and Stein [ReSt26] derived that bound for \(n\) large in terms of \(k\) from their dense-graph case of Erdős–Sós. For the one-vertex tree, \(R_k(T) \leq 2\).
theorem erdos_557 :
∃ c : ℕ, ∀ (k n : ℕ) (T : SimpleGraph (Fin n)), T.IsTree →
multicolourGraphRamsey k T ≤ k * n + c
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/557.lean, line 53.
Erdos557.erdos_557.variants.explicit
Solved: stated here; a Lean proof is at https://github.com/zhangjun725/erdos557/blob/c4e0ab13027f8bb50defade11cf8a53c7b8b0ba9/Erdos557/Basic.lean#L147.
The explicit bound \(R_k(T) \leq k(n-2)+3\) for every \(k\) and every tree \(T\) on \(n \geq 2\) vertices. The problem page states this bound for \(n\) sufficiently large in terms of \(k\).
The Lean statement uses natural-number subtraction, so for \(n = 1\) it reads \(R_k(T) \leq 3\), which also holds (the one-vertex tree has \(R_k(T) \leq 2\)). With ordinary subtraction the displayed formula would be false for \(n = 1\) and \(k \geq 3\).
theorem erdos_557.variants.explicit (k n : ℕ) (T : SimpleGraph (Fin n)) (hT : T.IsTree) :
multicolourGraphRamsey k T ≤ k * (n - 2) + 3
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/557.lean, line 69.
Erdos557.erdos_557.variants.tight
Solved: stated here; a Lean proof is at https://github.com/zhangjun725/erdos557/blob/828ad6fdb5d0f1a72b8dcd812f4c91c285570ff6/Erdos557/Tight.lean#L108.
The best-possible bound \(R_k(T) \leq k(n-2)+2\) for every \(k\) and every tree \(T\) on \(n \geq 2\) vertices, attained by stars. It follows from the sharp form of the Erdős–Sós theorem (a graph on \(m\) vertices with more than \((n-2)m/2\) edges contains every tree on \(n\) vertices) by the pigeonhole principle.
theorem erdos_557.variants.tight (k n : ℕ) (hn : 2 ≤ n) (T : SimpleGraph (Fin n))
(hT : T.IsTree) : multicolourGraphRamsey k T ≤ k * (n - 2) + 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/557.lean, line 82.
Erdos557.erdos_557.variants.tight_odd
Solved: stated here; a Lean proof is at https://github.com/zhangjun725/erdos557/blob/828ad6fdb5d0f1a72b8dcd812f4c91c285570ff6/Erdos557/Tight.lean#L114.
When \(n\) is odd and \(k \geq 2\) is even, \(R_k(T) \leq k(n-2)+1\) for every tree \(T\) on \(n\) vertices, again attained by stars: with \(m = k(n-2)+1\) some colour class has at least \((n-2)m/2\) edges, and \((n-2)m\) is odd, so it has more than \((n-2)m/2\) edges.
theorem erdos_557.variants.tight_odd (k n : ℕ) (hk : 0 < k) (hke : Even k) (hn : 2 ≤ n)
(hno : Odd n) (T : SimpleGraph (Fin n)) (hT : T.IsTree) :
multicolourGraphRamsey k T ≤ k * (n - 2) + 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/557.lean, line 94.
Sources
TheoremErdős Problem 559#
References: - erdosproblems.com/559 - [Be83b] Beck, József, On size Ramsey number of paths, trees, and circuits. I. J. Graph Theory (1983), 115-129. - [FrPi87] Friedman, J. and Pippenger, N., Expanding graphs contain all small trees. Combinatorica (1987), 71-76. - [HKL95] Haxell, P. E. and Kohayakawa, Y. and Łuczak, T., The induced size-Ramsey number of cycles. Combin. Probab. Comput. (1995), 217-239. - [RoSz00] Rödl, Vojtěch and Szemerédi, Endre, On size Ramsey numbers of graphs with bounded degree. Combinatorica (2000), 257-262. - [Ti22b] Tikhomirov, K., On bounded degree graphs with large size-Ramsey numbers. arXiv:2210.05818 (2022). - [DrPe22] N. Draganić and K. Petrova, Size-Ramsey numbers of graphs with maximum degree three. arXiv:2207.05048 (2022).
Quoted from FormalConjectures/ErdosProblems/559.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/559.
The file states 6 research or textbook statements: 6 solved.
Erdos559.erdos_559
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos559.lean#L1275.
Let \(\hat{R}(G)\) denote the size Ramsey number, the minimal number of edges \(m\) such that there is a graph \(H\) with \(m\) edges that is Ramsey for \(G\).
If \(G\) has \(n\) vertices and maximum degree \(d\) then prove that
\[\hat{R}(G)\ll_d n.\]This was disproved for \(d=3\) by Rödl and Szemerédi [RoSz00], who constructed a graph on \(n\) vertices with maximum degree \(3\) such that \(\hat{R}(G)\gg n(\log n)^{c}\) for some absolute constant \(c>0\).
theorem erdos_559 :
¬ ∀ d : ℕ, ∃ C : ℝ, ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
G.maxDegree ≤ d → (sizeRamsey G G : ℝ) ≤ C * Fintype.card V
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/559.lean, line 60.
Erdos559.erdos_559.variants.degree_three
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos559.lean#L1275.
Rödl and Szemerédi [RoSz00] disproved the linear bound already for maximum degree \(3\).
theorem erdos_559.variants.degree_three :
¬ ∃ C : ℝ, ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
G.maxDegree ≤ 3 → (sizeRamsey G G : ℝ) ≤ C * Fintype.card V
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/559.lean, line 70.
Erdos559.erdos_559.variants.rodl_szemeredi
Solved: stated here without proof.
Rödl and Szemerédi [RoSz00] constructed, for infinitely many \(n\), a graph on \(n\) vertices with maximum degree \(3\) such that \(\hat{R}(G)\gg n(\log n)^{c}\) for some absolute constant \(c>0\).
theorem erdos_559.variants.rodl_szemeredi :
∃ c > (0 : ℝ), ∃ C > 0, ∃ᶠ n : ℕ in atTop, ∃ G : SimpleGraph (Fin n),
G.maxDegree ≤ 3 ∧ C * n * (log n) ^ c ≤ sizeRamsey G G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/559.lean, line 80.
Erdos559.erdos_559.variants.tikhomirov
Solved: stated here without proof.
Tikhomirov [Ti22b] improved this to \(\hat{R}(G)\gg n\exp(c\sqrt{\log n})\).
theorem erdos_559.variants.tikhomirov :
∃ c > 0, ∃ C > 0, ∃ᶠ n : ℕ in atTop, ∃ G : SimpleGraph (Fin n),
G.maxDegree ≤ 3 ∧ C * n * exp (c * √(log n)) ≤ sizeRamsey G G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/559.lean, line 88.
Erdos559.erdos_559.variants.trees
Solved: stated here without proof.
Friedman and Pippenger [FrPi87] proved the linear bound when \(G\) is a tree.
theorem erdos_559.variants.trees (d : ℕ) :
∃ C : ℝ, ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
G.IsTree → G.maxDegree ≤ d → (sizeRamsey G G : ℝ) ≤ C * Fintype.card V
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/559.lean, line 96.
Erdos559.erdos_559.variants.draganic_petrova
Solved: stated here without proof.
The best known upper bound for graphs of maximum degree \(3\) is \(\hat{R}(G)\leq n^{3/2+o(1)}\), due to Draganić and Petrova [DrPe22].
theorem erdos_559.variants.draganic_petrova (ε : ℝ) (hε : 0 < ε) :
∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
G.maxDegree ≤ 3 → (sizeRamsey G G : ℝ) ≤ (n : ℝ) ^ (3 / 2 + ε : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/559.lean, line 105.
Sources
TheoremErdős Problem 560#
References: - erdosproblems.com/560 - [EFRS82] Erdős, P. and Faudree, R. J. and Rousseau, C. C. and Schelp, R. H., Ramsey numbers for brooms. Proceedings of the thirteenth Southeastern conference on combinatorics, graph theory and computing (1982), 283-293. - [ErRo93] Erdős, P. and Rousseau, C. C., The size Ramsey number of a complete bipartite graph. Discrete Math. (1993), 259-262. - [EFRS78b] Erdős, P. and Faudree, R. J. and Rousseau, C. C. and Schelp, R. H., The size Ramsey number. Period. Math. Hungar. (1978), 145-161. - [NeRo78] Nešetřil, J. and Rödl, V., The structure of critical Ramsey graphs. Acta Math. Acad. Sci. Hungar. (1978), 295-300. - [CFW23] Conlon, D. and Fox, J. and Wigderson, Y., Three early problems on size Ramsey numbers. Combinatorica (2023), 743-768.
Quoted from FormalConjectures/ErdosProblems/560.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/560.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos560.erdos_560
Open: stated without proof.
Let \(\hat{R}(G)\) denote the size Ramsey number, the minimal number of edges \(m\) such that there is a graph \(H\) with \(m\) edges such that in any \(2\)-colouring of the edges of \(H\) there is a monochromatic copy of \(G\).
Determine
\[\hat{R}(K_{n,n}),\]where \(K_{n,n}\) is the complete bipartite graph with \(n\) vertices in each component.
theorem erdos_560 : erdos_560.answer = (fun n : ℕ ↦ r̂(n))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/560.lean, line 61.
Erdos560.erdos_560.variants.lower_bound
Solved: stated here without proof.
The lower bound (which holds for \(n\geq 6\)) was proved by Erdős and Rousseau [ErRo93]:
\[\frac{1}{60}n^22^n\lt \hat{R}(K_{n,n}).\]
theorem erdos_560.variants.lower_bound :
∀ (n : ℕ), 6 ≤ n → (1 / 60 : ℝ) * (n : ℝ) ^ 2 * 2 ^ n < r̂(n)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/560.lean, line 69.
Erdos560.erdos_560.variants.upper_bound
Solved: stated here without proof.
The upper bound was proved by Erdős, Faudree, Rousseau, and Schelp [EFRS78b] and Nešetřil and Rödl [NeRo78]:
\[\hat{R}(K_{n,n})\lt \frac{3}{2}n^32^n.\]We require \(n\geq 1\) because the strict inequality fails for the empty graph.
theorem erdos_560.variants.upper_bound :
∀ (n : ℕ), 1 ≤ n → (r̂(n) : ℝ) < (3 / 2 : ℝ) * (n : ℝ) ^ 3 * 2 ^ n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/560.lean, line 80.
Erdos560.erdos_560.variants.conlon_fox_wigderson
Open: stated without proof.
Conlon, Fox, and Wigderson [CFW23] conjecture that
\[\hat{R}(K_{s,t})\asymp s^2t2^s\]for all \(s\leq t\), and so in particular we should have
\[\hat{R}(K_{n,n})\asymp n^32^n.\]
theorem erdos_560.variants.conlon_fox_wigderson :
(fun n : ℕ ↦ (r̂(n) : ℝ)) =Θ[atTop] (fun n : ℕ ↦ (n : ℝ) ^ 3 * 2 ^ n)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/560.lean, line 91.
Sources
TheoremErdős Problem 561#
References: - erdosproblems.com/561 - [BEFRS78] Burr, S. A. and Erdős, P. and Faudree, R. J. and Rousseau, C. C. and Schelp, R. H., Ramsey-minimal graphs for multiple copies. Nederl. Akad. Wetensch. Indag. Math. (1978), 187-195.
Quoted from FormalConjectures/ErdosProblems/561.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/561.
The file states 1 research or textbook statement: 1 open.
Erdos561.erdos_561
Open: stated without proof.
Let \(\hat{R}(G)\) denote the size Ramsey number, the minimal number of edges \(m\) such that there is a graph \(H\) with \(m\) edges such that in any \(2\)-colouring of the edges of \(H\) there is a monochromatic copy of \(G\).
Let \(F_1\) and \(F_2\) be the union of stars. More precisely, let \(F_1=\cup_{i\leq s}K_{1,n_i}\) and \(F_2=\cup_{j\leq t}K_{1,m_j}\) with \(n_1\geq\cdots\geq n_s\geq1\) and \(m_1\geq\cdots\geq m_t\geq1\). Prove that
\[\hat{R}(F_1,F_2)=\sum_{2\leq k\leq s+t}l_k\]where
\[l_k=\max\{n_i+m_j-1:i+j=k\}.\]The unions are vertex-disjoint, and \(s,t\geq1\). Lean indices start at zero, so the condition \(i+j=k\) is represented by \((i+1)+(j+1)=k\).
theorem erdos_561 :
∀ (s t : ℕ), 1 ≤ s → 1 ≤ t →
∀ (n : Fin s → ℕ) (m : Fin t → ℕ),
Antitone n → Antitone m → (∀ i, 1 ≤ n i) → (∀ j, 1 ≤ m j) →
sizeRamsey F(s, n) F(t, m) =
∑ k ∈ Finset.Icc 2 (s + t),
((Finset.univ : Finset (Fin s × Fin t)).filter
(fun p ↦ (p.1.val + 1) + (p.2.val + 1) = k)).sup
(fun p ↦ n p.1 + m p.2 - 1)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/561.lean, line 58.
Sources
TheoremErdős Problem 562#
Reference: erdosproblems.com/562
Quoted from FormalConjectures/ErdosProblems/562.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/562.
The file states 1 research or textbook statement: 1 open.
Erdos562.erdos_562
Open: stated without proof.
Let \(R_r(n)\) denote the \(r\)-uniform hypergraph Ramsey number: the minimal \(m\) such that if we \(2\)-colour all edges of the complete \(r\)-uniform hypergraph on \(m\) vertices then there must be some monochromatic copy of the complete \(r\)-uniform hypergraph on \(n\) vertices.
Prove that, for \(r \ge 3\),
\[ \log_{r-1} R_r(n) \asymp_r n, \]where \(\log_{r-1}\) denotes the \((r-1)\)-fold iterated logarithm.
theorem erdos_562 :
∀ r ≥ 3, (fun n ↦ log^[r - 1] (hypergraphRamsey r n)) =Θ[atTop] (fun n ↦ (n : ℝ))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/562.lean, line 43.
Sources
TheoremErdős Problem 563#
References: - erdosproblems.com/563 - [Er90b] Erdős, Paul, Problems and results on graphs and hypergraphs: similarities and differences. Mathematics of Ramsey theory (1990), 12-28.
Quoted from FormalConjectures/ErdosProblems/563.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/563.
The file states 1 research or textbook statement: 1 open.
Erdos563.erdos_563
Open: stated without proof.
Let \(F(n,\alpha)\) denote the smallest \(m\) such that there exists a \(2\)-colouring of the edges of \(K_n\) so that every \(X\subseteq [n]\) with \(\lvert X\rvert\geq m\) contains more than \(\alpha \binom{\lvert X\rvert}{2}\) many edges of each colour.
Prove that, for every \(0\leq \alpha < 1/2\),
\[F(n,\alpha)\sim c_\alpha\log n\]for some constant \(c_\alpha\) depending only on \(\alpha\).
This problem is #39 in Ramsey Theory in the graphs problem collection.
theorem erdos_563 :
∀ (α : ℝ), 0 ≤ α → α < 1 / 2 →
∃ (c : ℝ), 0 < c ∧
Tendsto (fun n : ℕ => (F n α : ℝ) / Real.log n) atTop (nhds c)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/563.lean, line 67.
Sources
TheoremErdős Problem 564#
Reference: erdosproblems.com/564
Quoted from FormalConjectures/ErdosProblems/564.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/564.
The file states 1 research or textbook statement: 1 open.
Erdos564.erdos_564
Open: stated without proof.
Let \(R_3(n)\) be the minimal \(m\) such that if the edges of the \(3\)-uniform hypergraph on \(m\) vertices are \(2\)-coloured then there is a monochromatic copy of the complete \(3\)-uniform hypergraph on \(n\) vertices.
Is there some constant \(c>0\) such that
\[ R_3(n) \geq 2^{2^{cn}}? \]
theorem erdos_564 :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (2 : ℝ) ^ (2 : ℝ) ^ (c * n) ≤ hypergraphRamsey 3 n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/564.lean, line 41.
Sources
TheoremErdős Problem 566#
References: - erdosproblems.com/566 - [EFRS93] Erdős, Faudree, Rousseau and Schelp, Ramsey size linear graphs. Combin. Probab. Comput. (1993), 389-399.
Quoted from FormalConjectures/ErdosProblems/566.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/566.
The file states 1 research or textbook statement: 1 open.
Erdos566.erdos_566
Open: stated without proof.
Let \(G\) be such that any subgraph on \(k\) vertices has at most \(2k-3\) edges. Is it true that, if \(H\) has \(m\) edges and no isolated vertices, then \(R(G,H) \ll m\)?
In other words: if \(G\) is sparse (every induced subgraph on \(k\) vertices has \(≤ 2k-3\) edges), is \(G\) Ramsey size linear?
theorem erdos_566 :
∀ (p : ℕ) (G : SimpleGraph (Fin p)),
(∀ S : Finset (Fin p), 2 ≤ S.card → (G.induce S).edgeSet.ncard ≤ 2 * S.card - 3) →
G.IsRamseySizeLinear
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/566.lean, line 43.
Sources
TheoremErdős Problem 567#
Let \(G\) be either \(Q_3\) or \(K_{3,3}\) or \(H_5\) (the last formed by adding two vertex-disjoint chords to \(C_5\)). Is it true that, if \(H\) has \(m\) edges and no isolated vertices, then
\[ R(G,H) \ll m? \]In other words, is \(G\) Ramsey size linear? A special case of Problem 566.
Reference: erdosproblems.com/567
[EFRS93] Erdős, Faudree, Rousseau and Schelp, Ramsey size linear graphs. Combin. Probab. Comput. (1993), 389-399.
Quoted from FormalConjectures/ErdosProblems/567.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/567.
The file states 3 research or textbook statements: 3 open.
Erdos567.erdos_567.parts.i
Open: stated without proof.
Erdős Problem 567 (Q3)
Is \(Q_3\) (the 3-dimensional hypercube) Ramsey size linear?
theorem erdos_567.parts.i : IsRamseySizeLinear Q3
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/567.lean, line 60.
Erdos567.erdos_567.parts.ii
Open: stated without proof.
Erdős Problem 567 (K33)
Is \(K_{3,3}\) Ramsey size linear?
theorem erdos_567.parts.ii : IsRamseySizeLinear K33
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/567.lean, line 69.
Erdos567.erdos_567.parts.iii
Open: stated without proof.
Erdős Problem 567 (H5)
Is \(H_5\) (\(C_5\) with two vertex-disjoint chords) Ramsey size linear?
theorem erdos_567.parts.iii : IsRamseySizeLinear H5
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/567.lean, line 78.
Sources
TheoremErdős Problem 568#
References: - erdosproblems.com/568 - [EFRS93] Erdős, P. and Faudree, R. J. and Rousseau, C. C. and Schelp, R. H., Ramsey size linear graphs. Combin. Probab. Comput. (1993), 389-399.
Quoted from FormalConjectures/ErdosProblems/568.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/568.
The file states 1 research or textbook statement: 1 open.
Erdos568.erdos_568
Open: stated without proof.
Let \(G\) be a graph such that \(R(G,T_n)\ll n\) for any tree \(T_n\) on \(n\) vertices and \(R(G,K_n)\ll n^2\). Is it true that, for any \(H\) with \(m\) edges and no isolated vertices,
\[R(G,H)\ll m?\]In other words, is \(G\) Ramsey size linear?
This problem is #33 in Ramsey Theory in the graphs problem collection.
theorem erdos_568 :
∀ (V : Type) [Fintype V] (G : SimpleGraph V),
(∃ c₁ > (0 : ℝ), ∀ (n : ℕ) (T : SimpleGraph (Fin n)),
T.IsTree → (SimpleGraph.graphRamsey G T : ℝ) ≤ c₁ * n) →
(∃ c₂ > (0 : ℝ), ∀ (n : ℕ),
(SimpleGraph.graphRamsey G (SimpleGraph.completeGraph (Fin n)) : ℝ) ≤ c₂ * (n : ℝ) ^ 2) →
G.IsRamseySizeLinear
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/568.lean, line 43.
Sources
TheoremErdős Problem 569#
References: - erdosproblems.com/569 - [EFRS93] Erdős, Paul and Faudree, R. J. and Rousseau, C. C. and Schelp, R. H., Ramsey size linear graphs. Combin. Probab. Comput. (1993), 389-399.
Quoted from FormalConjectures/ErdosProblems/569.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/569.
The file states 1 research or textbook statement: 1 open.
Erdos569.erdos_569
Open: stated without proof.
Let \(k\geq 1\). What is the best possible \(c_k\) such that
\[R(C_{2k+1},H)\leq c_k m\]for any graph \(H\) on \(m\) edges without isolated vertices?
This problem is #34 in Ramsey Theory in the graphs problem collection.
theorem erdos_569 :
∀ (k : ℕ) (hk : 1 ≤ k),
sInf {C : ℝ | 0 < C ∧
∀ (m : ℕ) (W : Type) [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj],
(∀ v, 0 < H.degree v) →
H.edgeSet.ncard = m →
(SimpleGraph.graphRamsey (SimpleGraph.cycleGraph (2 * k + 1)) H : ℝ) ≤ C * m} =
erdos_569.answer k
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/569.lean, line 43.
Sources
TheoremErdős Problem 570#
References: - erdosproblems.com/570 - [EFRS93] Erdős, P. and Faudree, R. J. and Rousseau, C. C. and Schelp, R. H., Ramsey size linear graphs. Combin. Probab. Comput. (1993), 389-399. - [GoKl94] Goddard, W. and Kleitman, D. J., An upper bound for the Ramsey numbers \(r(K_3,G)\). Discrete Math. (1994), 177-182. - [Si91] Sidorenko, A. F., An upper bound on the Ramsey number \(r(K_3,G)\) depending only on the size of the graph \(G\). J. Graph Theory (1991), 15-17. - [Ja99] Jayawardene, C. J., Ramsey numbers related to small cycles. University of Memphis (1999). - [CFMPP26] Cambie, S., Freschi, A., Morawski, P., Petrova, K. and Pokrovskiy, A., Ramsey number of a cycle versus a graph of a given size. arXiv:2601.10238 (2026).
Quoted from FormalConjectures/ErdosProblems/570.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/570.
The file states 1 research or textbook statement: 1 solved.
Erdos570.erdos_570
Solved: stated here without proof.
Let \(k\geq 3\). Is it true that, if \(m\) is sufficiently large, for any graph \(H\) on \(m\) edges without isolated vertices,
\[R(C_k,H) \leq 2m+\left\lfloor\frac{k-1}{2}\right\rfloor?\]This was proved for even \(k\) by Erdős, Faudree, Rousseau, and Schelp [EFRS93]. This was proved for \(k=3\) independently by Goddard and Kleitman [GoKl94] and Sidorenko [Si91]. This was proved for \(k=5\) by Jayawardene [Ja99]. Finally it was proved for all odd \(k\geq 7\) by Cambie, Freschi, Morawski, Petrova, and Pokrovskiy [CFMPP26].
This problem is #35 in Ramsey Theory in the graphs problem collection.
theorem erdos_570 :
∀ (k : ℕ) (hk : 3 ≤ k),
∀ᶠ (m : ℕ) in atTop,
∀ (W : Type) [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj],
(∀ v, 0 < H.degree v) →
H.edgeSet.ncard = m →
SimpleGraph.graphRamsey (SimpleGraph.cycleGraph k) H ≤ 2 * m + (k - 1) / 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/570.lean, line 55.
Sources
TheoremErdős Problem 571#
References: - erdosproblems.com/571 - Formal Lean proof - [BuCo18] Bukh, Boris and Conlon, David, Rational exponents in extremal graph theory. J. Eur. Math. Soc. (JEMS) (2018), 1747-1757. - [CJL21] Conlon, David and Janzer, Oliver and Lee, Joonkyung, More on the extremal number of subdivisions. Combinatorica (2021), 465-494. - [CoJa22] Conlon, David and Janzer, Oliver, Rational exponents near two. Adv. Comb. (2022), Paper No. 9, 10. - [Er78] Erdős, Paul, Problems and results in combinatorial analysis and combinatorial number theory. Proceedings of the Ninth Southeastern Conference on Combinatorics, Graph Theory, and Computing (Florida Atlantic Univ., Boca Raton, Fla., 1978) (1978), 29-40. - [JJM20] Jiang, Tao and Jiang, Zilin and Ma, Jie, Negligible obstructions and Turán exponents. arXiv:2007.02975 (2020). - [JMY22] Jiang, Tao and Ma, Jie and Yepremyan, Liana, On Turán exponents of bipartite graphs. Combin. Probab. Comput. (2022), 333-344. - [JiQi20] Jiang, Tao and Qiu, Yu, Turán numbers of bipartite subdivisions. SIAM J. Discrete Math. (2020), 556-570. - [JiQi23] Jiang, Tao and Qiu, Yu, Many Turán exponents via subdivisions. Combin. Probab. Comput. (2023), 134-150. - [KKL21] Kang, Dong Yeap and Kim, Jaehoon and Liu, Hong, On the rational Turán exponents conjecture. J. Combin. Theory Ser. B (2021), 149-172.
Quoted from FormalConjectures/ErdosProblems/571.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/571.
The file states 1 research or textbook statement: 1 solved.
Erdos571.erdos_571
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/2f055a777231a73a305b379e993c37f00ed5a66b/problems/571/Erdos571.lean.
Show that for any rational \(\alpha \in [1,2)\) there exists a bipartite graph \(G\) such that
\[\mathrm{ex}(n;G)\asymp n^{\alpha}.\]The proof constructs balanced rooted models for all rational parameters. Its upper-bound closure replaces old edges by paths of arbitrary length, adds two color-class hubs, and commutes with positive rooted powers.
theorem erdos_571 :
∀ α : ℚ, 1 ≤ α → α < 2 →
∃ q : ℕ, ∃ G : SimpleGraph (Fin q), G.IsBipartite ∧
Asymptotics.IsTheta atTop
(fun n : ℕ => (extremalNumber n G : ℝ))
(fun n : ℕ => (n : ℝ) ^ (α : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/571.lean, line 62.
Sources
TheoremErdős Problem 572#
References: - erdosproblems.com/572 - [Er64c] Erdős, P., Extremal problems in graph theory. Theory of Graphs and its Applications (1964), 29-36. - [BoSi74] Bondy, J. A. and Simonovits, M., Cycles of even length in graphs. J. Combin. Theory Ser. B (1974), 97-105. - [LUW95] Lazebnik, F., Ustimenko, V. A. and Woldar, A. J., A new series of dense graphs of high girth. Bull. Amer. Math. Soc. (N.S.) (1995), 73-79.
Quoted from FormalConjectures/ErdosProblems/572.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/572.
The file states 1 research or textbook statement: 1 open.
Erdos572.erdos_572
Open: stated without proof.
Show that for \(k\geq 3\)
\[\mathrm{ex}(n;C_{2k})\gg n^{1+\frac{1}{k}}.\]This problem is #46 in Extremal Graph Theory in the graphs problem collection.
theorem erdos_572 (k : ℕ) (hk : 3 ≤ k) :
∃ c > (0 : ℝ), ∀ᶠ (n : ℕ) in atTop,
c * (n : ℝ) ^ (1 + 1 / (k : ℝ)) ≤
(SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph (2 * k)) : ℝ)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/572.lean, line 46.
Sources
TheoremErdős Problem 573#
References: - erdosproblems.com/573 - [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. - [Er75] Erdős, P., Some recent progress on extremal problems in graph theory. Congr. Numer. (1975), 3-14. - [ErSi82] Erdős, P. and Simonovits, M., Compactness results in extremal graph theory. Combinatorica (1982), 275-288. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [KST54] Kővári, T. and Sós, V. T. and Turán, P., On a problem of K. Zarankiewicz. Colloq. Math. (1954), 50-57.
Quoted from FormalConjectures/ErdosProblems/573.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/573.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos573.erdos_573
Open: stated without proof.
Is it true that
\[\mathrm{ex}(n;\{C_3,C_4\})\sim (n/2)^{3/2}?\]A problem of Erdős and Simonovits. This problem is asking whether the threshold is the same as for forbidding \(C_4\) and all odd cycles (see
erdos_573.variants.kst) if one only forbids the odd cycle of length \(3\). See also [574] for the general case, and [765] for \(\mathrm{ex}(n;C_4)\).This problem is #48 in Extremal Graph Theory in the graphs problem collection.
theorem erdos_573 :
(fun n : ℕ ↦ (cycleExtremalNumber {3, 4} n : ℝ)) ~[atTop]
fun n : ℕ ↦ ((n : ℝ) / 2) ^ (3 / 2 : ℝ)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/573.lean, line 65.
Erdos573.erdos_573.variants.c4_c5
Solved: stated here without proof.
Erdős and Simonovits [ErSi82] proved that
\[\mathrm{ex}(n;\{C_4,C_5\})=(n/2)^{3/2}+O(n).\]The source writes an equality; only the upper bound is stated here.
theorem erdos_573.variants.c4_c5 :
∃ C : ℝ, ∀ᶠ n : ℕ in atTop,
(cycleExtremalNumber {4, 5} n : ℝ) ≤ ((n : ℝ) / 2) ^ (3 / 2 : ℝ) + C * n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/573.lean, line 77.
Erdos573.erdos_573.variants.kst
Solved: stated here without proof.
Kővári, Sós, and Turán [KST54] proved that the extremal number of edges for containing either \(C_4\) or an odd cycle of any length is \(\sim (n/2)^{3/2}\), that is,
\[\mathrm{ex}(n;\{C_4, C_3, C_5, C_7, \ldots\})\sim (n/2)^{3/2}.\]Equivalently, the maximum number of edges of a bipartite \(C_4\)-free graph on \(n\) vertices is \(\sim (n/2)^{3/2}\). The attribution follows erdosproblems.com; the matching lower bound comes from finite-geometry constructions.
theorem erdos_573.variants.kst :
(fun n : ℕ ↦ (cycleExtremalNumber ({4} ∪ {k | Odd k ∧ 3 ≤ k}) n : ℝ)) ~[atTop]
fun n : ℕ ↦ ((n : ℝ) / 2) ^ (3 / 2 : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/573.lean, line 91.
Sources
TheoremErdős Problem 577#
References: - erdosproblems.com/577 - [Wa10] Wang, Hong, Proof of the Erdős-Faudree conjecture on quadrilaterals. Graphs Combin. (2010), 833-877. DOI
Quoted from FormalConjectures/ErdosProblems/577.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/577.
The file states 1 research or textbook statement: 1 solved.
Erdos577.erdos_577
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos577.lean.
If \(G\) is a graph with \(4k\) vertices and minimum degree at least \(2k\) then \(G\) contains \(k\) vertex-disjoint \(4\)-cycles.
A conjecture of Erdős and Faudree. Proved by Wang [Wa10].
theorem erdos_577 (k : ℕ) (G : SimpleGraph (Fin (4 * k)))
(hG : 2 * k ≤ G.minDegree) :
∃ cycles : Fin k → (cycleGraph 4).Copy G,
Pairwise fun i j => Disjoint (Set.range (fun v => cycles i v))
(Set.range (fun v => cycles j v))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/577.lean, line 46.
Sources
TheoremErdős Problem 578#
References: - erdosproblems.com/578 - [Ri00] Riordan, Oliver, Spanning subgraphs of random graphs. Combin. Probab. Comput. (2000), 125-148. DOI
Quoted from FormalConjectures/ErdosProblems/578.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/578.
The file states 2 research or textbook statements: 2 solved.
Erdos578.erdos_578
Solved: stated here without proof.
If \(G\) is a random graph on \(2^d\) vertices, including each edge with probability \(1/2\), then \(G\) almost surely contains a copy of \(Q_d\) (the \(d\)-dimensional hypercube with \(2^d\) vertices and \(d2^{d-1}\) many edges).
A conjecture of Erdős and Bollobás. Solved by Riordan [Ri00], who in fact proved this with any edge-probability \(>1/4\).
Here almost surely means that the probability tends to \(1\) as \(d\to\infty\).
theorem erdos_578 :
Tendsto (fun d : ℕ =>
binomialRandom (Fin d → Bool) ⟨1 / 2, by norm_num⟩
{G | (hypercube d).IsContained G}) atTop (nhds 1)
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/578.lean, line 46.
Erdos578.erdos_578.variants.riordan
Solved: stated here without proof.
For every fixed edge-probability \(p>1/4\), the probability that a random graph on \(2^d\) vertices contains a copy of \(Q_d\) tends to \(1\) as \(d\to\infty\). Proved by Riordan [Ri00].
theorem erdos_578.variants.riordan (p : unitInterval) (hp : (1 : ℝ) / 4 < p) :
Tendsto (fun d : ℕ =>
binomialRandom (Fin d → Bool) p {G | (hypercube d).IsContained G})
atTop (nhds 1)
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/578.lean, line 55.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.