Erdős Problem 532 to Erdős Problem 552
TheoremErdős Problem 532#
References: - erdosproblems.com/532 - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (1973), 117-138. - [Er75b] Erdős, Paul, Problems and results in combinatorial number theory. Journées Arithmétiques de Bordeaux (1975), 295-310. - [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (1977), 43-72. - [Hi74] Hindman, Neil, Finite sums from sequences within cells of a partition of \(\mathbb{N}\). J. Combinatorial Theory Ser. A (1974), 1-11.
Quoted from FormalConjectures/ErdosProblems/532.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/532.
The file states 1 research or textbook statement: 1 solved.
Erdos532.erdos_532
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos532.lean.
If \(\mathbb{N}\) is 2-coloured then is there some infinite set \(A\subseteq \mathbb{N}\) such that all finite subset sums
\[ \sum_{n\in S}n\](as \(S\) ranges over all non-empty finite subsets of \(A\)) are monochromatic?
Asked by Graham and Rothschild. Proved by Hindman [Hi74] (for any number of colours).
theorem erdos_532 :
∀ (c : ℕ → Fin 2),
∃ A : Set ℕ, A.Infinite ∧
∃ color : Fin 2,
∀ S : Finset ℕ, S.Nonempty → ↑S ⊆ A →
c (∑ n ∈ S, n) = color
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/532.lean, line 44.
Sources
TheoremErdős Problem 533#
References: - erdosproblems.com/533 - [EHSSS94] P. Erdős, A. Hajnal, M. Simonovits, V. T. Sós and E. Szemerédi, Turán-Ramsey theorems and \(K_p\)-independence numbers, Combin. Probab. Comput. 3 (1994), 297–325. - [ErRo62] P. Erdős and C. A. Rogers, The construction of certain graphs, Canad. J. Math. 14 (1962), 702–707. - [BaLe13] J. Balogh and J. Lenz, On the Ramsey–Turán numbers of graphs and hypergraphs, Israel J. Math. 194 (2013), 45–68. - [LRSS21] H. Liu, C. Reiher, M. Sharifzadeh and K. Staden, Geometric constructions for Ramsey–Turán theory, arXiv:2103.10423 (2021).
Quoted from FormalConjectures/ErdosProblems/533.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/533.
The file states 5 research or textbook statements: 5 solved. It also has 1 test statement, counted here but not shown.
Erdos533.erdos_533
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos533.lean#L2922.
Let \(\delta > 0\). If \(n\) is sufficiently large and \(G\) is a graph on \(n\) vertices with no \(K_5\) and at least \(\delta n^2\) edges, must \(G\) contain a set of \(\gg_\delta n\) vertices spanning no triangle?
Equivalently, writing \(\mathrm{RT}_3(n, K_5, m)\) for the maximum number of edges of a \(K_5\)-free graph on \(n\) vertices in which every triangle-free vertex set has fewer than \(m\) vertices (the triangle Ramsey–Turán number), is
\[\delta_3(5) = \lim_{\epsilon \to 0} \lim_{n \to \infty} \frac{\mathrm{RT}_3(n, K_5, \epsilon n)}{n^2} = 0?\]This is a problem of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94], who proved \(\delta_3(5) \leq 1/12\) and the analogous \(\delta_3(4) = 0\), and observed \(\delta_3(7) \geq 1/4\) via a construction of Erdős and Rogers [ErRo62].
The answer is no: Balogh and Lenz [BaLe13] disproved it by showing \(\delta_3(5) > 0\), and the exact value \(\delta_3(5) = 1/12\) was determined by the matching lower-bound construction of Liu, Reiher, Sharifzadeh, and Staden [LRSS21] (see
erdos_533.variants.lrss_lower).
theorem erdos_533 :
¬ ∀ δ : ℝ, 0 < δ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
∀ G : SimpleGraph (Fin n), G.CliqueFree 5 →
δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
∃ S : Finset (Fin n), c * n ≤ (S.card : ℝ) ∧
G.CliqueFreeOn (S : Set (Fin n)) 3
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/533.lean, line 66.
Erdos533.erdos_533.variants.ehsss_upper
Solved: stated here without proof.
The upper bound \(\delta_3(5) \leq 1/12\) of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94]: for every \(\epsilon > 0\) there is a \(\delta > 0\) such that for all sufficiently large \(n\), every \(K_5\)-free graph \(G\) on \(n\) vertices in which every triangle-free vertex set has at most \(\delta n\) vertices has at most \((1/12 + \epsilon)n^2\) edges.
theorem erdos_533.variants.ehsss_upper (ε : ℝ) (hε : 0 < ε) :
∃ δ : ℝ, 0 < δ ∧ ∀ᶠ n : ℕ in atTop,
∀ G : SimpleGraph (Fin n), G.CliqueFree 5 →
(∀ S : Finset (Fin n),
G.CliqueFreeOn (S : Set (Fin n)) 3 → (S.card : ℝ) ≤ δ * n) →
(G.edgeFinset.card : ℝ) ≤ (1 / 12 + ε) * n ^ 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/533.lean, line 82.
Erdos533.erdos_533.variants.lrss_lower
Solved: stated here without proof.
The matching lower bound \(\delta_3(5) \geq 1/12\), from the construction of Liu, Reiher, Sharifzadeh, and Staden [LRSS21] (improving the earlier \(\delta_3(5) > 0\) of Balogh and Lenz [BaLe13]): for every \(\epsilon, \delta > 0\) and all sufficiently large \(n\) there is a \(K_5\)-free graph \(G\) on \(n\) vertices in which every triangle-free vertex set has at most \(\delta n\) vertices, yet which has at least \((1/12 - \epsilon)n^2\) edges. In particular this refutes
erdos_533.
theorem erdos_533.variants.lrss_lower (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
∀ᶠ n : ℕ in atTop,
∃ G : SimpleGraph (Fin n), G.CliqueFree 5 ∧
(∀ S : Finset (Fin n),
G.CliqueFreeOn (S : Set (Fin n)) 3 → (S.card : ℝ) ≤ δ * n) ∧
(1 / 12 - ε) * (n : ℝ) ^ 2 ≤ G.edgeFinset.card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/533.lean, line 100.
Erdos533.erdos_533.variants.delta_four_eq_zero
Solved: stated here without proof.
The contrasting positive result \(\delta_3(4) = 0\) of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94]: the \(K_4\) analogue of
erdos_533is true. For every \(\delta > 0\) there is a \(c > 0\) such that for all sufficiently large \(n\), every \(K_4\)-free graph \(G\) on \(n\) vertices with at least \(\delta n^2\) edges contains a triangle-free vertex set of size at least \(c n\).
theorem erdos_533.variants.delta_four_eq_zero :
∀ δ : ℝ, 0 < δ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
∀ G : SimpleGraph (Fin n), G.CliqueFree 4 →
δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
∃ S : Finset (Fin n), c * n ≤ (S.card : ℝ) ∧
G.CliqueFreeOn (S : Set (Fin n)) 3
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/533.lean, line 117.
Erdos533.erdos_533.variants.delta_seven_ge_quarter
Solved: stated here without proof.
The observation \(\delta_3(7) \geq 1/4\) of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94], via a construction of Erdős and Rogers [ErRo62]: for every \(\epsilon, \delta > 0\) and all sufficiently large \(n\) there is a \(K_7\)-free graph \(G\) on \(n\) vertices in which every triangle-free vertex set has at most \(\delta n\) vertices, yet which has at least \((1/4 - \epsilon)n^2\) edges.
theorem erdos_533.variants.delta_seven_ge_quarter (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
∀ᶠ n : ℕ in atTop,
∃ G : SimpleGraph (Fin n), G.CliqueFree 7 ∧
(∀ S : Finset (Fin n),
G.CliqueFreeOn (S : Set (Fin n)) 3 → (S.card : ℝ) ≤ δ * n) ∧
(1 / 4 - ε) * (n : ℝ) ^ 2 ≤ G.edgeFinset.card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/533.lean, line 134.
Sources
TheoremErdős Problem 534#
References: - erdosproblems.com/534 - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [AhKh96] Ahlswede, Rudolf and Khachatrian, Levon H., Sets of integers with pairwise common divisor and a factor from a specified set of primes. Acta Arith. (1996), 259--276.
Quoted from FormalConjectures/ErdosProblems/534.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/534.
The file states 1 research or textbook statement: 1 solved.
Erdos534.erdos_534
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos534.lean#L39.
What is the largest possible subset \(A\subseteq\{1,\ldots,N\}\) which contains \(N\) such that \(\mathrm{gcd}(a,b)>1\) for all \(a\neq b\in A\)?
Erdős conjectured that if \(N=q_1^{k_1}\cdots q_r^{k_r}\) (where \(q_1\lt \cdots \lt q_r\) are distinct primes) then the maximum is achieved by, for some \(1\leq j\leq r\), those integers in \([1,N]\) which are a multiple of at least one of \(\{2q_1,\ldots,2q_j,q_1\cdots q_j\}\).
This conjecture was proved by Ahlswede and Khachatrian [AhKh96].
theorem erdos_534 (N : ℕ) (hN : 2 ≤ N) :
∃ q ∈ N.primeFactors, IsAdmissible N (ahlswedeKhachatrian N q) ∧
maxCard N = (ahlswedeKhachatrian N q).card
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/534.lean, line 70.
Sources
TheoremErdős Problem 535#
References: - erdosproblems.com/535 - [Er64] P. Erdős, On a problem in elementary number theory and a combinatorial problem. Math. Comp. (1964), 644–646. - [AbHa70] H. L. Abbott and D. Hanson, An extremal problem in number theory. Bull. London Math. Soc. (1970), 324–326. - [Er73] P. Erdős, Problems and results on combinatorial number theory, in A Survey of Combinatorial Theory, North-Holland, 1973.
Quoted from FormalConjectures/ErdosProblems/535.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/535.
The file states 7 research or textbook statements: 3 open and 4 solved.
Erdos535.erdos_535
Open: stated without proof.
Let \(r \geq 3\), and let \(f_r(N)\) denote the size of the largest subset of \(\{1,\ldots,N\}\) such that no subset of size \(r\) has the same pairwise greatest common divisor between all elements. Erdős [Er64] proved that \(f_3(N) > N^{c/\log\log N}\) for some constant \(c > 0\), and conjectured this should also be an upper bound; here we state the conjectural upper bound for all \(r \geq 3\).
See also [536].
theorem erdos_535 : ∀ r ≥ 3, ∃ c > (0 : ℝ),
∀ᶠ (N : ℕ) in atTop,
(f r N : ℝ) ≤ (N : ℝ) ^ (c / log (log (N : ℝ)))
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/535.lean, line 76.
Erdos535.erdos_535.variants.first_open_case
Open: stated without proof.
The first open case of Erdős Problem 535 is \(r = 3\): there should exist \(c > 0\) such that \(f_3(N) \leq N^{c/\log\log N}\) for all sufficiently large \(N\).
theorem erdos_535.variants.first_open_case : ∃ c > (0 : ℝ),
∀ᶠ (N : ℕ) in atTop,
(f 3 N : ℝ) ≤ (N : ℝ) ^ (c / log (log (N : ℝ)))
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/535.lean, line 86.
Erdos535.erdos_535.variants.erdos_upper_bound
Solved: stated here without proof.
Erdős [Er64] proved that \(f_r(N) \leq N^{3/4+o(1)}\) for all \(r \geq 3\).
theorem erdos_535.variants.erdos_upper_bound {r : ℕ} (hr : 3 ≤ r) :
∀ ε > (0 : ℝ), ∀ᶠ (N : ℕ) in atTop,
(f r N : ℝ) ≤ (N : ℝ) ^ ((3 : ℝ) / 4 + ε)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/535.lean, line 93.
Erdos535.erdos_535.variants.lower_bound
Solved: stated here without proof.
Erdős [Er64] proved that \(f_3(N) > N^{c/\log\log N}\) for some constant \(c > 0\).
theorem erdos_535.variants.lower_bound : ∃ c > (0 : ℝ),
∀ᶠ (N : ℕ) in atTop,
(N : ℝ) ^ (c / log (log (N : ℝ))) ≤ (f 3 N : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/535.lean, line 100.
Erdos535.erdos_535.variants.abbott_hanson
Solved: stated here without proof.
Abbott and Hanson [AbHa70] improved Erdős's upper bound to \(f_r(N) \leq N^{1/2+o(1)}\) for all \(r \geq 3\).
theorem erdos_535.variants.abbott_hanson {r : ℕ} (hr : 3 ≤ r) :
∀ ε > (0 : ℝ), ∀ᶠ (N : ℕ) in atTop,
(f r N : ℝ) ≤ (N : ℝ) ^ ((1 : ℝ) / 2 + ε)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/535.lean, line 108.
Erdos535.erdos_535.variants.sunflower_strong
Open: stated without proof.
Erdős [Er73] records that Abbott pointed out the ordinary sunflower conjecture does not seem to suffice here. The stronger auxiliary conjecture uses \(Ω(n)=k\), i.e. prime factors counted with multiplicity; this stronger statement would imply the conjectured upper bound for \(f_r(N)\).
theorem erdos_535.variants.sunflower_strong {r : ℕ} (hr : 3 ≤ r) :
∃ c_r > (0 : ℝ),
∀ k : ℕ, ∀ A : Finset ℕ,
AllBigOmega k A →
NoConstantPairwiseGcdCoprimeSubsets r A →
(A.card : ℝ) ≤ c_r ^ k
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/535.lean, line 120.
Erdos535.erdos_535.variants.sunflower_erdos_rado
Solved: stated here without proof.
For the stronger \(Ω(n)=k\) variant above, the Erdős–Rado method gives the weaker bound \(c_r^k \cdot k!\); see Erdős [Er73].
theorem erdos_535.variants.sunflower_erdos_rado {r : ℕ} (hr : 3 ≤ r) :
∃ c_r > (0 : ℝ),
∀ k : ℕ, ∀ A : Finset ℕ,
AllBigOmega k A →
NoConstantPairwiseGcdCoprimeSubsets r A →
(A.card : ℝ) ≤ c_r ^ k * (Nat.factorial k)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/535.lean, line 133.
Sources
TheoremErdős Problem 536#
Reference: erdosproblems.com/536
Quoted from FormalConjectures/ErdosProblems/536.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/536.
The file states 1 research or textbook statement: 1 open.
Erdos536.erdos_536
Open: stated without proof.
Let \(\epsilon>0\) and \(N\) be sufficiently large. Is it true that if \(A\subseteq \{1,\ldots,N\}\) has size at least \(\epsilon N\) then there must be distinct \(a,b,c\in A\) such that
\[[a, b]=[b, c]=[a, c],\]where \([\cdot, \cdot]\) denotes the least common multiple?
theorem erdos_536 :
∀ᵉ (ε > (0: ℝ)), ∀ᶠ N in atTop,
∀ (A : Finset ℕ), A ⊆ Icc 1 N → (ε * (N : ℝ)) ≤ (A.card : ℝ) →
∃ᵉ (a ∈ A) (b ∈ A) (c ∈ A),
# {a, b, c} = 3 ∧ a.lcm b = b.lcm c ∧ b.lcm c = a.lcm c
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/536.lean, line 39.
Sources
TheoremErdős Problem 537#
References: - erdosproblems.com/537 - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.
Quoted from FormalConjectures/ErdosProblems/537.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/537.
The file states 1 research or textbook statement: 1 solved.
Erdos537.erdos_537
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos537.lean.
Let \(\epsilon>0\) and \(N\) be sufficiently large. If \(A\subseteq \{1,\ldots,N\}\) has \(\lvert A\rvert \geq \epsilon N\) then must there exist \(a_1,a_2,a_3\in A\) and distinct primes \(p_1,p_2,p_3\) such that
\[a_1p_1=a_2p_2=a_3p_3?\]A positive answer would imply [536].
Erdős describes a construction of Ruzsa which disproves this: consider the set of all squarefree numbers of the shape \(p_1\cdots p_r\) where \(p_{i+1}>2p_i\) for \(1\leq i\lt r\). This set has positive density, and hence if \(A\) is its intersection with \((N/2,N)\) then \(\lvert A\rvert \gg N\) for all large \(N\). Suppose now that \(p_1a_1=p_2a_2=p_3a_3\) where \(a_i\in A\) and \(p_1,p_2,p_3\) are distinct primes. Without loss of generality we may assume that \(a_2>a_3\) and hence \(p_2\lt p_3\), and so since \(p_2p_3\mid a_1\in A\) we must have \(2\lt p_3/p_2\). On the other hand \(p_3/p_2=a_2/a_3\in (1,2)\), a contradiction.
theorem erdos_537 :
¬ ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop,
∀ A ⊆ Finset.Icc 1 N, (A.card : ℝ) ≥ ε * N →
∃ a₁ ∈ A, ∃ a₂ ∈ A, ∃ a₃ ∈ A, ∃ p₁ p₂ p₃ : ℕ,
p₁.Prime ∧ p₂.Prime ∧ p₃.Prime ∧
p₁ ≠ p₂ ∧ p₁ ≠ p₃ ∧ p₂ ≠ p₃ ∧
a₁ * p₁ = a₂ * p₂ ∧ a₂ * p₂ = a₃ * p₃
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/537.lean, line 53.
Sources
TheoremErdős Problem 538#
Reference: erdosproblems.com/538
Quoted from FormalConjectures/ErdosProblems/538.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/538.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos538.erdos_538
Open: stated without proof.
Let \(r\geq 2\) and suppose that \(A\subseteq\{1,\ldots,N\}\) is such that, for any \(m\), there are at most \(r\) solutions to \(m=pa\) where \(p\) is prime and \(a\in A\). Give the best possible upper bound for \(\sum_{n\in A}\frac{1}{n}\).
Erdős observed that \(\sum_{n\in A}\frac{1}{n}\ll r\frac{\log N}{\log\log N}\), and the order
Θ_r(log N / loglog N)is known (seeerdos_538.matching_order). The best possible upper bound is the asymptotic size of the largest reciprocal summaxMass r Nover admissibleA.
theorem erdos_538 :
∀ r : ℕ, 2 ≤ r → maxMass r ~[atTop] erdos_538.answer r
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/538.lean, line 61.
Erdos538.erdos_538.matching_order
Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-538/Research/FinalMatchingOrder.lean.
The reciprocal sum has matching order
Θ_r(log N / loglog N): an explicit upper bound for every admissibleA, together with a witnessing construction achieving the same order. This pins the order (up to the one iterated-logarithm factor) but not the best possible upper bound asked for inerdos_538.
theorem erdos_538.matching_order (r N : ℕ) (hr : 2 ≤ r) (hN : 2 ≤ N) :
(∀ A : Finset ℕ, Admissible r N A →
Real.log (Real.log (N + 1)) * (reciprocalMass A : ℝ) ≤
2 * r * (1 + Real.log (N * N))) ∧
(∃ A : Finset ℕ, Admissible r N A ∧
Real.log (N + 1) ≤
4 + (8192 * (Nat.log 2 (Nat.log 2 N) + 1) : ℝ) * (reciprocalMass A : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/538.lean, line 73.
Sources
TheoremErdős Problem 539#
In this problem, a function \(h : \mathbb{N} \to\mathbb{N}\) is defined maximally by a specified counting property.
The problem asks to estimate \(h(n)\). This has been interpreted here as asking for \(\Theta(h(n))\). The principal version includes the unknown function
erdos_539.answer. On the other hand, the best known upper bound is \(n^{2/3}\) and the best known lower bound is \(\sqrt{n}\) so we also provide these candidates as variants. Moreover, it suffices to show \(O(h(n))\) and \(O(\sqrt{n})\) respectively for each, so further variants are provided for those.In the source paper [Er73], Erdős also remarks that it should not be too difficult to determine \(\lim_{n\to\infty}\log(h(n))/\log(n)\). This does not appear on the website, and it is not clear whether this remains open, but we include it here either way.
References: - erdosproblems.com/539 - [GR99] Granville, A., & Roesler, F. (1999). The Set of Differences of a Given Set. The American Mathematical Monthly, 106(4), 338–344. - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138. - [Sc+26] Schmitt, J., Gehrunger, T., Dekoninck, J., Bérczi, G., Kreitner, U., Price, L., & Holmes, D. (2026). ProofCouncil: An LLM Agent for Solving Open Mathematical Problems. arXiv:2607.09474, Appendix A, Theorem A.1.
Quoted from FormalConjectures/ErdosProblems/539.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/539.
The file states 8 research or textbook statements: 1 open and 7 solved.
Erdos539.erdos_539
Open: stated without proof.
Let \(h(n)\) be maximal such that, for any set \(A\subseteq \mathbb{N}\) of size \(n\), the set
\[\left\{ \frac{a}{(a,b)}: a,b\in A\right\}\]has size at least \(h(n)\). Estimate \(h(n)\).
theorem erdos_539 :
(fun n ↦ (cofactorThreshold n : ℝ)) =Θ[atTop] erdos_539.answer
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/539.lean, line 66.
Erdos539.erdos_539.variants.sq
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-539-sqrt-disproof/blob/f4b14f9ef32c111162d3fd587e1c65b27a1524d5/lean/Erdos539SqrtFC.lean#L41-L44.
Let \(h(n)\) be maximal such that, for any set \(A\subseteq \mathbb{N}\) of size \(n\), the set
\[\left\{ \frac{a}{(a,b)}: a,b\in A\right\}\]has size at least \(h(n)\). Is \(h(n) = \Theta(\sqrt{n})\)?
theorem erdos_539.variants.sq :
¬ ((fun n ↦ (cofactorThreshold n : ℝ)) =Θ[atTop] fun n ↦ √n)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/539.lean, line 77.
Erdos539.erdos_539.variants.sq_isBigO
Solved: stated here without proof.
Erdős and Szemerédi proved that
\[n^{1/2} \ll h(n)\].
theorem erdos_539.variants.sq_isBigO :
(fun n : ℕ ↦ √n) =O[atTop] fun n ↦ (cofactorThreshold n : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/539.lean, line 83.
Erdos539.erdos_539.variants.isBigO_sq
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-539-sqrt-disproof/blob/f4b14f9ef32c111162d3fd587e1c65b27a1524d5/lean/Erdos539SqrtFC.lean#L36-L39.
Is \(h(n) = O(\sqrt{n})\)?
theorem erdos_539.variants.isBigO_sq :
¬ ((fun n ↦ (cofactorThreshold n : ℝ)) =O[atTop] fun n ↦ √n)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/539.lean, line 92.
Erdos539.erdos_539.variants.sq_cube_root
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-539-formal-conjectures/blob/79897cf9241390eb168572f4a481e29e0e64b5f7/lean/Erdos539/FC.lean#L282-L296.
Let \(h(n)\) be maximal such that, for any set \(A\subseteq \mathbb{N}\) of size \(n\), the set
\[\left\{ \frac{a}{(a,b)}: a,b\in A\right\}\]has size at least \(h(n)\). Is \(h(n) = \Theta(n^{2/3})\)? The answer is negative; see [Sc+26, Theorem A.1] and the linked Lean proof.
theorem erdos_539.variants.sq_cube_root :
¬ ((fun n ↦ (cofactorThreshold n : ℝ)) =Θ[atTop]
fun n ↦ (n : ℝ) ^ ((2 : ℝ) / 3))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/539.lean, line 104.
Erdos539.erdos_539.variants.isBigO_sq_cube_root
Solved: stated here without proof.
Granville and Roesler [GR99] showed that
\[h(n)\ll n^{2/3}\].
theorem erdos_539.variants.isBigO_sq_cube_root :
(fun n ↦ (cofactorThreshold n : ℝ)) =O[atTop] fun n ↦ (n : ℝ) ^ ((2 : ℝ) / 3)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/539.lean, line 111.
Erdos539.erdos_539.variants.sq_cube_root_isBigO
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-539-formal-conjectures/blob/79897cf9241390eb168572f4a481e29e0e64b5f7/lean/Erdos539/FC.lean#L282-L296.
This lower bound is false; see [Sc+26, Theorem A.1] and the linked Lean proof.
theorem erdos_539.variants.sq_cube_root_isBigO :
¬ ((fun n : ℕ ↦ (n : ℝ) ^ ((2 : ℝ) / 3)) =O[atTop]
fun n ↦ (cofactorThreshold n : ℝ))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/539.lean, line 120.
Erdos539.erdos_539.variants.limit
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-539-formal-conjectures/blob/79897cf9241390eb168572f4a481e29e0e64b5f7/lean/Erdos539/FC.lean#L282-L296.
From [Er73]: The determination of
\[ \lim_{n\to\infty}\frac{\log(h(n))}{\log(n)} \]will perhaps be not too difficult. The limit is \(1/2\); see [Sc+26, Theorem A.1] and the linked Lean proof.
theorem erdos_539.variants.limit :
atTop.Tendsto
(fun n ↦ Real.log (cofactorThreshold n) / Real.log n)
erdos_539.variants.limit.answer
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/539.lean, line 138.
Sources
TheoremErdős Problem 540#
References: - erdosproblems.com/540 - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Ol68] Olson, John E., An addition theorem modulo {\(p\)}. J. Combinatorial Theory (1968), 45--52. - [Ba12] Balandraud, Éric, An addition theorem and maximal zero-sum free sets in \(\mathbb{Z}/p\mathbb{Z}\). Israel J. Math. (2012), 405-429. - [HaZe96] Hamidoune, Yahya Ould and Zémor, Gilles, On zero-free subset sums. Acta Arith. (1996), 143--152. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [ErHe64] Erdős, P. and Heilbronn, H., On the addition of residue classes mod \(p\). Acta Arith. (1964), 149--159. - [Sz70] Szemerédi, E., On a conjecture of Erdős and Heilbronn. Acta Arith. (1970), 227-229.
Quoted from FormalConjectures/ErdosProblems/540.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/540.
The file states 1 research or textbook statement: 1 solved.
Erdos540.erdos_540
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos540.lean.
Is it true that if \(A\subseteq \mathbb{Z}/N\mathbb{Z}\) has size \(\gg N^{1/2}\) then there exists some non-empty \(S\subseteq A\) such that \(\sum_{n\in S}n\equiv 0\pmod{N}\)?
Szemerédi proved the answer is yes, in fact for arbitrary finite abelian groups.
theorem erdos_540 :
∃ C : ℝ, 0 < C ∧
∀ (N : ℕ), 0 < N → ∀ A : Finset (ZMod N),
C * Real.sqrt N ≤ A.card →
HasZeroSubsetSum A
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/540.lean, line 59.
Sources
TheoremErdős Problem 541#
References: - erdosproblems.com/541 - [ErSz76] Erdős, E. and Szemerédi, E., On a problem of Graham. Publ. Math. Debrecen (1976), 123--127. - [GHW10] Gao, Weidong and Hamidoune, Yahya Ould and Wang, Guoqing, Distinct length modular zero-sum subsequences: a proof of Graham's conjecture. J. Number Theory (2010), 1425--1431.
Quoted from FormalConjectures/ErdosProblems/541.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/541.
The file states 3 research or textbook statements: 3 solved.
Erdos541.erdos_541
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos541.lean.
Let \(a_1, \dots, a_p\) be (not necessarily distinct) residues modulo a prime \(p\), such that there exists some \(r\) so that if \(S \subseteq [p]\) is non-empty and
\[\sum_{i \in S} a_i \equiv 0 \pmod{p}\]then \(|S| = r\).
Must there be at most two distinct residues amongst the \(a_i\)?
This was formalized in Lean by Alexeev using Aristotle and ChatGPT.
theorem erdos_541 : (∀ p, Fact p.Prime → ∀ (a : Fin p → ZMod p),
(∃ r, ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) →
(Set.range a).ncard ≤ 2)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/541.lean, line 49.
Erdos541.erdos_541.variants.general_moduli
Solved: stated here without proof.
Gao, Hamidoune, and Wang [GHW10] solved this for all moduli
p(not necessarily prime).
theorem erdos_541.variants.general_moduli (p : ℕ) (a : Fin p → ZMod p)
(ha₀ : ∃ r, ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) :
(Set.range a).ncard ≤ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/541.lean, line 56.
Erdos541.erdos_541.variants.large_primes
Solved: stated here without proof.
This was proved by Erdős and Szemerédi [ErSz76] for p sufficiently large.
theorem erdos_541.variants.large_primes : ∀ᶠ p in atTop, p.Prime → ∀ a : Fin p → ZMod p,
(∃ r, ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) →
(Set.range a).ncard ≤ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/541.lean, line 63.
Sources
TheoremErdős Problem 542#
References: - erdosproblems.com/542 - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180. - [ScSz59] Schinzel, A. and Szekeres, G., Sur un problème de M. Paul Erdős. Acta Sci. Math. (Szeged) (1959), 221-229. - [Ch96] Chen, Yong-Gao, On a problem of P. Erdős. Acta Sci. Math. (Szeged) (1996), 101--114.
Quoted from FormalConjectures/ErdosProblems/542.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/542.
The file states 8 research or textbook statements: 2 open and 6 solved.
Erdos542.erdos_542.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos542.lean#L2114.
Is it true that if \(A\subseteq\{1,\ldots,n\}\) is a set such that \([a,b]>n\) for all \(a\neq b\), where \([a,b]\) is the least common multiple, then
\[\sum_{a\in A}\frac{1}{a}\leq \frac{31}{30}?\]The answer is yes, proved by Schinzel and Szekeres [ScSz59]. The bound is best possible as \(A=\{2,3,5\}\) demonstrates.
theorem erdos_542.parts.i :
∀ (n : ℕ) (A : Finset ℕ), IsLcmFree n A → ∑ a ∈ A, (1 : ℝ) / a ≤ 31 / 30
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/542.lean, line 62.
Erdos542.erdos_542.variants.sharp
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos542.lean#L2114.
The bound \(31/30\) is attained by \(A=\{2,3,5\}\) (with \(n=5\)).
theorem erdos_542.variants.sharp :
IsLcmFree 5 {2, 3, 5} ∧ ∑ a ∈ ({2, 3, 5} : Finset ℕ), (1 : ℝ) / a = 31 / 30
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/542.lean, line 70.
Erdos542.erdos_542.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos542.lean#L2114.
Is it true that if \(A\subseteq\{2,\ldots,n\}\) is a set such that \([a,b]>n\) for all \(a\neq b\), then there must be \(\gg n\) many \(m\leq n\) which are not divisible by any \(a\in A\)?
The answer is no, proved by Schinzel and Szekeres [ScSz59].
The element \(1\) is excluded: \(A=\{1\}\) satisfies the hypothesis and leaves no such \(m\), so without this restriction the answer would be negative for a trivial reason.
theorem erdos_542.parts.ii :
¬ ∃ c > 0, ∀ (n : ℕ) (A : Finset ℕ), IsLcmFree n A → 1 ∉ A →
c * n ≤ ((uncovered n A).card : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/542.lean, line 86.
Erdos542.erdos_542.variants.schinzel_szekeres
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos542.lean#L2114.
Schinzel and Szekeres [ScSz59] proved that, for any \(\epsilon>0\), there are sets \(A\subseteq\{2,\ldots,n\}\) as in the problem with \(o(n)\) many uncovered \(m\leq n\) and for which \(\sum_{a\in A}\frac{1}{a}>1-\epsilon\).
theorem erdos_542.variants.schinzel_szekeres :
∀ ε > 0, ∀ δ > 0, ∃ (n : ℕ) (A : Finset ℕ), IsLcmFree n A ∧ 1 ∉ A ∧
((uncovered n A).card : ℝ) ≤ δ * n ∧ 1 - ε < ∑ a ∈ A, (1 : ℝ) / a
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/542.lean, line 99.
Erdos542.erdos_542.variants.log_power
Solved: stated here without proof.
Schinzel and Szekeres [ScSz59] proved that there are examples \(A\subseteq\{2,\ldots,n\}\) with at most \(n/(\log n)^c\) many such \(m\), for some real constant \(c>0\).
theorem erdos_542.variants.log_power : ∃ c > (0 : ℝ), ∃ᶠ n : ℕ in atTop, ∃ A : Finset ℕ,
IsLcmFree n A ∧ 1 ∉ A ∧ ((uncovered n A).card : ℝ) ≤ n / (log n) ^ c
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/542.lean, line 109.
Erdos542.erdos_542.variants.chen
Solved: stated here without proof.
Chen [Ch96] has proved that if \(n>172509\) then
\[\sum_{a\in A}\frac{1}{a}< \frac{1}{3}+\frac{1}{4}+\frac{1}{5}+\frac{1}{7}+\frac{1}{11}.\]
theorem erdos_542.variants.chen (n : ℕ) (hn : 172509 < n) (A : Finset ℕ) (hA : IsLcmFree n A) :
∑ a ∈ A, (1 : ℝ) / a < 1 / 3 + 1 / 4 + 1 / 5 + 1 / 7 + 1 / 11
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/542.lean, line 118.
Erdos542.erdos_542.variants.one_add_little_o
Open: stated without proof.
In [Er73] Erdős further speculates that in fact
\[\sum_{a\in A}\frac{1}{a}\leq 1+o(1),\]where the \(o(1)\) term \(\to 0\) as \(n\to \infty\).
theorem erdos_542.variants.one_add_little_o :
∃ o : ℕ → ℝ, Tendsto o atTop (nhds 0) ∧
∀ (n : ℕ) (A : Finset ℕ), IsLcmFree n A → ∑ a ∈ A, (1 : ℝ) / a ≤ 1 + o n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/542.lean, line 128.
Erdos542.erdos_542.variants.only_two
Open: stated without proof.
In [Er98] Erdős mentions that he, Schinzel, and Szekeres conjectured that \(2,3,5\) and \(3,4,5,7,11\) are the only two sequences for which the sum is \(>1\).
theorem erdos_542.variants.only_two :
∀ (n : ℕ) (A : Finset ℕ), IsLcmFree n A → 1 < ∑ a ∈ A, (1 : ℝ) / a →
A = {2, 3, 5} ∨ A = {3, 4, 5, 7, 11}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/542.lean, line 138.
Sources
TheoremErdős Problem 544#
References: - erdosproblems.com/544
Quoted from FormalConjectures/ErdosProblems/544.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/544.
The file states 2 research or textbook statements: 2 open.
Erdos544.erdos_544.parts.i
Open: stated without proof.
Show that
\[R(3,k+1)-R(3,k)\to\infty\]as \(k\to \infty\).
A problem of Erdős and Sós. This problem is #8 in Ramsey Theory in the graphs problem collection.
theorem erdos_544.parts.i :
Tendsto (fun k : ℕ ↦ (SimpleGraph.classicalRamsey 3 (k + 1) : ℝ) -
(SimpleGraph.classicalRamsey 3 k : ℝ)) atTop atTop
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/544.lean, line 42.
Erdos544.erdos_544.parts.ii
Open: stated without proof.
Similarly, prove or disprove that
\[R(3,k+1)-R(3,k)=o(k).\]
theorem erdos_544.parts.ii :
(fun k : ℕ ↦ (SimpleGraph.classicalRamsey 3 (k + 1) : ℝ) -
(SimpleGraph.classicalRamsey 3 k : ℝ)) =o[atTop] (fun k : ℕ ↦ (k : ℝ))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/544.lean, line 52.
Sources
TheoremErdős Problem 545#
References: - erdosproblems.com/545 - [ErGr75] Erdős, P. and Graham, R. L., On partition theorems for finite graphs. Infinite and finite sets (1975), 515-527. - [Er84b] Erdős, P., On some problems in graph theory, combinatorial analysis and combinatorial number theory. Graph theory and combinatorics (Cambridge, 1983) (1984), 1-17.
Quoted from FormalConjectures/ErdosProblems/545.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/545.
The file states 1 research or textbook statement: 1 open.
Erdos545.erdos_545
Open: stated without proof.
Let \(m\) be sufficiently large and let \(G\) be a graph with \(m\) edges and no isolated vertices. Is the Ramsey number \(R(G)\) maximised when \(G\) is 'as complete as possible'? That is, if \(m=\binom{n}{2}+t\) edges with \(0\leq t < n\) then is
\[R(G)\leq R(H),\]where \(H\) is the graph formed by connecting a new vertex to \(t\) of the vertices of \(K_n\)?
A question of Erdős and Graham. The restriction to sufficiently large \(m\) excludes the small counterexamples recorded on the source page.
This problem is #10 in Ramsey Theory in the graphs problem collection.
theorem erdos_545 :
∀ᶠ m : ℕ in atTop, ∀ (n t : ℕ), t < n → m = n.choose 2 + t →
∀ (V : Type) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj],
(∀ v, 0 < G.degree v) →
G.edgeSet.ncard = m →
SimpleGraph.diagonalGraphRamsey G ≤
SimpleGraph.diagonalGraphRamsey (knPlusTEdges n t)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/545.lean, line 65.
Sources
TheoremErdős Problem 546#
References: - erdosproblems.com/546 - [Su11] Sudakov, B., A conjecture of Erdős on graph Ramsey numbers. Adv. Math. (2011), 3148-3155. - [AKS03] Alon, N., Krivelevich, M. and Sudakov, B., Turán numbers of bipartite graphs and Ramsey graphs of bounded degree. Combin. Probab. Comput. (2003), 477-483. - PALOMAR-2026-10-04-000010
Quoted from FormalConjectures/ErdosProblems/546.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/546.
The file states 1 research or textbook statement: 1 solved.
Erdos546.erdos_546
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/7caa4144741e10f96cf79d6f7313a0efd9a18b67/erdos-546/Proofs/OriginalStatement546.lean#L33.
Let \(G\) be a graph with no isolated vertices and \(m\) edges. Is it true that
\[R(G) \leq 2^{O(m^{1/2})}?\]This is true, and was proved by Sudakov [Su11].
This problem is #11 in Ramsey Theory in the graphs problem collection.
theorem erdos_546 :
∃ C > (0 : ℝ), ∀ (m : ℕ) (V : Type) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj],
(∀ v, 0 < G.degree v) →
G.edgeSet.ncard = m →
(SimpleGraph.diagonalGraphRamsey G : ℝ) ≤ 2 ^ (C * Real.sqrt m)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/546.lean, line 45.
Sources
TheoremErdős Problem 547#
References: - erdosproblems.com/547 - [Bu74] Burr, S. A., Generalized Ramsey theory for graphs—a survey. Graphs and combinatorics (Proc. Capital Conf., George Washington Univ., Washington, D.C., 1973) (1974), 52-75. - [Zh11] Zhao, Y., Proof of the \((n/2-n/2-n/2)\) conjecture for large \(n\). Electron. J. Combin. (2011), Paper 27, 61.
Quoted from FormalConjectures/ErdosProblems/547.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/547.
The file states 2 research or textbook statements: 2 solved.
Erdos547.erdos_547
Solved: stated here; a Lean proof is at https://github.com/zhangjun725/erdos557/blob/c4e0ab13027f8bb50defade11cf8a53c7b8b0ba9/Erdos557/Erdos547.lean#L84.
If \(T\) is a tree on \(n\) vertices then
\[R(T) \leq 2n-2.\]This problem is #14 in Ramsey Theory in the graphs problem collection.
Solved: the bound follows from the Erdős–Sós theorem (Erdős problem 548) by the pigeonhole principle, as noted on the problem page.
theorem erdos_547 :
∀ (n : ℕ) (hn : 2 ≤ n) (T : SimpleGraph (Fin n)),
T.IsTree → SimpleGraph.diagonalGraphRamsey T ≤ 2 * n - 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/547.lean, line 49.
Erdos547.erdos_547.variants.sufficiently_large
Solved: stated here without proof.
For sufficiently large \(n\), every tree \(T\) on \(n\) vertices satisfies \(R(T)\leq 2n-2\). Proved by Zhao [Zh11].
theorem erdos_547.variants.sufficiently_large :
∀ᶠ n : ℕ in atTop, ∀ T : SimpleGraph (Fin n),
T.IsTree → SimpleGraph.diagonalGraphRamsey T ≤ 2 * n - 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/547.lean, line 59.
Sources
TheoremErdős Problem 548#
References: - erdosproblems.com/548 - [BrDo96] Brandt, Stephan and Dobson, Edward, The Erdős-Sós conjecture for graphs of girth {\(5\)}. Discrete Math. (1996), 411-414. - [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. - [ErGa59] Erdős, P. and Gallai, T., On maximal paths and circuits of graphs. Acta Math. Acad. Sci. Hungar. (1959), 337-356 (unbound insert). - [SaWo97] Saclé, Jean-François and Woźniak, Mariusz, The Erdős-Sós conjecture for graphs without {\(C_4\)}. J. Combin. Theory Ser. B (1997), 367-372. - [WLL00] Wang, Min and Li, Guo-jun and Liu, Ai-de, A result of Erdős-Sós conjecture. Ars Combin. (2000), 123-127. - [YiLi04] Yin, Jian-hua and Li, Jiong-sheng, The Erdős-Sós conjecture for graphs whose complements contain no {\(C_4\)}. Acta Math. Appl. Sin. Engl. Ser. (2004), 397-400.
Quoted from FormalConjectures/ErdosProblems/548.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/548.
The file states 1 research or textbook statement: 1 solved.
Erdos548.erdos_548
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/4c355efbf8e90c2572aa8d0c8d6f3b4b43f011f4/problems/548/Erdos548.lean#L1182.
Let \(n\geq k+1\). Every graph on \(n\) vertices with at least \(\frac{k-1}{2}n+1\) edges contains every tree on \(k+1\) vertices.
theorem erdos_548 (n k : ℕ) (hk : k + 1 ≤ n) (G : SimpleGraph (Fin n))
(H : ((k : ℚ) - 1) / 2 * n + 1 ≤ (G.edgeSet.ncard : ℚ))
(T : SimpleGraph (Fin (k + 1))) (hT : T.IsTree) : T.IsContained G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/548.lean, line 52.
Sources
TheoremErdős Problem 549#
References: - erdosproblems.com/549 - [Bu74] Burr, S. A., Generalized Ramsey theory for graphs—a survey. Graphs and combinatorics (Proc. Capital Conf., George Washington Univ., Washington, D.C., 1973) (1974), 52-75. - [NSZ16] S. Norin and Y. R. Sun and Y. Zhao, Asymptotics of Ramsey numbers of double stars.
Quoted from FormalConjectures/ErdosProblems/549.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/549.
The file states 1 research or textbook statement: 1 solved.
Erdos549.erdos_549
Solved: stated here without proof.
If \(T\) is a tree which is a bipartite graph with \(k\) vertices in one class and \(2k\) vertices in the other class then
\[R(T)=4k-1.\]This is false: Norin, Sun, and Zhao [NSZ16] have proved that if \(T\) is the union of two stars on \(k\) and \(2k\) vertices, with an edge joining the centre of the two stars, then \(R(T)\geq (4.2-o(1))k\), and conjectured that \(R(T)=(4.2+o(1))k\).
This problem is #15 in Ramsey Theory in the graphs problem collection.
theorem erdos_549 :
¬ ∀ (k : ℕ) (hk : 2 ≤ k) (T : SimpleGraph (Fin k ⊕ Fin (2 * k))),
T.IsTree →
(∀ x₁ x₂, ¬ T.Adj (Sum.inl x₁) (Sum.inl x₂)) →
(∀ y₁ y₂, ¬ T.Adj (Sum.inr y₁) (Sum.inr y₂)) →
SimpleGraph.diagonalGraphRamsey T = 4 * k - 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/549.lean, line 46.
Sources
TheoremErdős Problem 550#
References: - erdosproblems.com/550 - [Ch77] Chvátal, V., Tree-complete graph Ramsey numbers. J. Graph Theory (1977), 93. - [Li26] Li, E., A Resolution of Erdős Problem 550 on Tree versus Complete Multipartite Ramsey Numbers, arXiv:2606.23659 (2026).
Quoted from FormalConjectures/ErdosProblems/550.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/550.
The file states 1 research or textbook statement: 1 solved.
Erdos550.erdos_550
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos550/Main.lean#L80.
Let \(m_1\leq\cdots\leq m_k\) and \(n\) be sufficiently large. If \(T\) is a tree on \(n\) vertices and \(G\) is the complete multipartite graph with vertex class sizes \(m_1,\ldots,m_k\) then prove that
\[R(T,G)\leq (\chi(G)-1)(R(T,K_{m_1,m_2})-1)+m_1.\]This problem is #16 in Ramsey Theory in the graphs problem collection.
Li [Li26] proved this, combining an off-Turán tree-embedding theorem with a compactness theorem for bounded-rank hypergraph obstructions. The linked formal proof states the bound for trees on an arbitrary finite vertex type and with
K_{m_1,m_2}written as a complete multipartite graph with two parts; the statement below is the special caseV = Fin n.
theorem erdos_550 :
∀ (k : ℕ) (hk : 2 ≤ k) (m : Fin k → ℕ) (hm : Monotone m)
(hm_pos : ∀ i, 0 < m i),
∀ᶠ n : ℕ in atTop,
∀ (T : SimpleGraph (Fin n)), T.IsTree →
SimpleGraph.graphRamsey T
(SimpleGraph.completeMultipartiteGraph (fun i ↦ Fin (m i))) ≤
(k - 1) * (SimpleGraph.graphRamsey T
(completeBipartiteGraph (Fin (m ⟨0, by omega⟩)) (Fin (m ⟨1, by omega⟩))) - 1) +
m ⟨0, by omega⟩
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/550.lean, line 51.
Sources
TheoremErdős Problem 551#
References: - erdosproblems.com/551 - [BoEr73] Bondy, J. A. and Erdős, P., Ramsey numbers for cycles in graphs. J. Combin. Theory Ser. B (1973), 46-54. - [Ni05] Nikiforov, V., The cycle-complete graph Ramsey numbers. Combin. Probab. Comput. (2005), 349-370. - [KLS21] Keevash, P., Long, E. and Skokan, J., Cycle-complete Ramsey numbers. Int. Math. Res. Not. IMRN (2021), 277-302.
Quoted from FormalConjectures/ErdosProblems/551.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/551.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos551.erdos_551
Open: stated without proof.
Prove that
\[R(C_k,K_n)=(k-1)(n-1)+1\]for \(k\geq n\geq 3\) (except when \(n=k=3\)).
Asked by Erdős, Faudree, Rousseau, and Schelp. This problem is #18 in Ramsey Theory in the graphs problem collection.
theorem erdos_551 :
∀ (k n : ℕ), 3 ≤ n → n ≤ k → ¬(n = 3 ∧ k = 3) →
SimpleGraph.graphRamsey (SimpleGraph.cycleGraph k)
(SimpleGraph.completeGraph (Fin n)) = (k - 1) * (n - 1) + 1
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/551.lean, line 48.
Erdos551.erdos_551.variants.sufficiently_large
Solved: stated here without proof.
For sufficiently large \(n\) and every \(k\geq n\), \(R(C_k,K_n)=(k-1)(n-1)+1\).
Keevash, Long, and Skokan [KLS21] have proved this identity when \(k\geq C\frac{\log n}{\log\log n}\) for some constant \(C\), thus establishing the conjecture for sufficiently large \(n\).
theorem erdos_551.variants.sufficiently_large :
∀ᶠ n : ℕ in atTop, ∀ k : ℕ, n ≤ k →
SimpleGraph.graphRamsey (SimpleGraph.cycleGraph k)
(SimpleGraph.completeGraph (Fin n)) = (k - 1) * (n - 1) + 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/551.lean, line 62.
Sources
TheoremErdős Problem 552#
References: - erdosproblems.com/552 - [BEFRS89] Burr, S. and Erdős, P. and Faudree, R. J. and Rousseau, C. C. and Schelp, R. H., Some complete bipartite graph-tree Ramsey numbers. Graph theory in memory of G. A. Dirac (Sandbjerg, 1985) (1989), 79-89. - [Ch97] Chen, G., A result on \(C_4\)-star Ramsey numbers. Discrete Mathematics 163 (1997), 243-246.
Quoted from FormalConjectures/ErdosProblems/552.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/552.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos552.erdos_552.parts.i
Open: stated without proof.
Determine the Ramsey number
\[R(C_4, S_n),\]where \(S_n=K_{1,n}\) is the star on \(n+1\) vertices.
A problem of Burr, Erdős, Faudree, Rousseau, and Schelp [BEFRS89].
This problem is #19 in Ramsey Theory in the graphs problem collection.
theorem erdos_552.parts.i :
∀ (n : ℕ),
SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4)
(completeBipartiteGraph (Fin 1) (Fin n)) =
erdos_552.parts.i.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/552.lean, line 48.
Erdos552.erdos_552.parts.ii
Open: stated without proof.
In particular, is it true that, for any \(c > 0\), there are infinitely many \(n\) such that
\[R(C_4, S_n) \leq n + \sqrt{n} - c?\]
theorem erdos_552.parts.ii :
∀ (c : ℝ), 0 < c →
Set.Infinite {n : ℕ |
(SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4)
(completeBipartiteGraph (Fin 1) (Fin n)) : ℝ) ≤ (n : ℝ) + Real.sqrt n - c}
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/552.lean, line 60.
Erdos552.erdos_552.variants.succ_le_add_two
Solved: stated here; a Lean proof is at https://github.com/agnt-gg/erdos-lean/blob/8e5972f4e6787049b168e5350b1a2badc9eb8bcd/Erdos/Erdos552.lean#L292.
Burr, Erdős, Faudree, Rousseau and Schelp also asked whether \(f(n + 1) \le f(n) + 2\) for all \(n\), where \(f(n) = R(C_4, S_n)\). Chen [Ch97] proved this for \(n \ge 1\). It fails for \(n = 0\), since \(R(C_4, S_1) = 4\) and \(R(C_4, S_0) = 1\).
theorem erdos_552.variants.succ_le_add_two (n : ℕ) (hn : 1 ≤ n) :
SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4)
(completeBipartiteGraph (Fin 1) (Fin (n + 1))) ≤
SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4)
(completeBipartiteGraph (Fin 1) (Fin n)) + 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/552.lean, line 75.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.