Erdős Problem 1182 to Erdős Problem 1199
TheoremErdős Problem 1182#
References: - erdosproblems.com/1182 - [Er78] Erdős, P., 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. PDF - [BEFRS80] Burr, S. A., Erdős, P., Faudree, R. J., Rousseau, C. C. and Schelp, R. H., An extremal problem in generalized Ramsey theory. Ars Combin. 10 (1980), 193-203. PDF - [Br96] Brandt, S., Expanding graphs and Ramsey numbers. Freie Universität Berlin, preprint A 96-24 (1996). - [BBH98] Brandt, S., Brinkmann, G. and Harmuth, T., All Ramsey numbers \(r(K_3,G)\) for connected graphs of order 9. Electron. J. Combin. 5 (1998), #R7. - [Ch77] Chvátal, V., Tree-complete graph Ramsey numbers. J. Graph Theory 1 (1977), 93. - [NiRo09] Nikiforov, V. and Rousseau, C. C., Ramsey goodness and beyond. Combinatorica 29 (2009), 227-262.
Quoted from FormalConjectures/ErdosProblems/1182.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/1182.
The file states 14 research or textbook statements: 2 open, 11 solved and 1 textbook result. It also has 1 API statement, counted here but not shown.
Erdos1182.erdos_1182.parts.i
Open: stated without proof.
Let \(f(n)\) be maximal such that there is a connected graph \(G\) with \(n\) vertices and \(f(n)\) edges such that
\[R(K_3,G)= 2n-1.\]Let \(F(n)\) be maximal such that every connected graph \(G\) with \(n\) vertices and \(\leq F(n)\) edges has
\[R(K_3,G)= 2n-1.\]Estimate \(f(n)\) and \(F(n)\). In particular, is it true that \(F(n)/n\to \infty\)?
This is the first part: estimate \(f(n)\). The problem is due to Burr, Erdős, Faudree, Rousseau and Schelp [BEFRS80] and appears in [Er78, p. 33]. We read "estimate" as the order of magnitude
=Θ. Burr, Erdős, Faudree, Rousseau and Schelp [BEFRS80, Theorem 2] proved \(n^{3/2}(\log n)^{1/2}\ll f(n)\ll n^{5/3}(\log n)^{2/3}\) (erdos_1182.variants.f_lower,erdos_1182.variants.f_upper).
theorem erdos_1182.parts.i :
(fun n : ℕ ↦ (f n : ℝ)) =Θ[atTop] erdos_1182.parts.i.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 108.
Erdos1182.erdos_1182.parts.ii
Solved: stated here without proof.
Let \(f(n)\) be maximal such that there is a connected graph \(G\) with \(n\) vertices and \(f(n)\) edges such that
\[R(K_3,G)= 2n-1.\]Let \(F(n)\) be maximal such that every connected graph \(G\) with \(n\) vertices and \(\leq F(n)\) edges has
\[R(K_3,G)= 2n-1.\]Estimate \(f(n)\) and \(F(n)\). In particular, is it true that \(F(n)/n\to \infty\)?
This is the second part: estimate \(F(n)\). As an order of magnitude,
=Θ, this is known: \(F(n)=\Theta(n)\), by \(F(n)\ge n-1\) (erdos_1182.variants.F_ge_pred, from Chvátal's theorem [Ch77]) and the linear upper bounds oferdos_1182.variants.brandtanderdos_1182.variants.nikiforov_rousseau. The finer question of the asymptotic behaviour of \(F(n)/n\) is open, seeerdos_1182.variants.brandt_expects.
theorem erdos_1182.parts.ii :
(fun n : ℕ ↦ (F n : ℝ)) =Θ[atTop] erdos_1182.parts.ii.answer
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 130.
Erdos1182.erdos_1182.parts.iii
Solved: stated here without proof.
Let \(f(n)\) be maximal such that there is a connected graph \(G\) with \(n\) vertices and \(f(n)\) edges such that
\[R(K_3,G)= 2n-1.\]Let \(F(n)\) be maximal such that every connected graph \(G\) with \(n\) vertices and \(\leq F(n)\) edges has
\[R(K_3,G)= 2n-1.\]Estimate \(f(n)\) and \(F(n)\). In particular, is it true that \(F(n)/n\to \infty\)?
This is the third part, asked in [BEFRS80, Section 5] and in [Er78, pp. 33-34], where Erdős says it seems certain. The answer is no: Brandt [Br96] proved \(F(n)\le 84n\) (as recorded on the problem page, see
erdos_1182.variants.brandt), and [NiRo09, Theorem 5.1] implies \(F(n)<50n\) for large \(n\) (seeerdos_1182.variants.nikiforov_rousseau).
theorem erdos_1182.parts.iii :
¬ Tendsto (fun n : ℕ ↦ (F n : ℝ) / n) atTop atTop
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 149.
Erdos1182.erdos_1182.variants.ramsey_ge
Textbook result, stated without proof.
It is trivial that \(R(K_3,G)\geq 2n-1\) for any connected graph \(G\) on \(n\) vertices ([BEFRS80, p. 193]).
theorem erdos_1182.variants.ramsey_ge {n : ℕ} (G : SimpleGraph (Fin n)) (hG : G.Connected) :
2 * n - 1 ≤ SimpleGraph.graphRamsey (⊤ : SimpleGraph (Fin 3)) G
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 158.
Erdos1182.erdos_1182.variants.chvatal
Solved: stated here without proof.
By a result of Chvátal [Ch77], \(R(K_3,T)=2n-1\) whenever \(T\) is a tree on \(n\) vertices (as stated in [BEFRS80, p. 193]).
theorem erdos_1182.variants.chvatal {n : ℕ} (T : SimpleGraph (Fin n)) (hT : T.IsTree) :
IsTriangleGood T
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 167.
Erdos1182.erdos_1182.variants.F_ge_pred
Solved: stated here without proof.
Every connected graph with at most \(n-1\) edges is a tree, so Chvátal's theorem [Ch77] gives \(F(n)\geq n-1\) ([BEFRS80, p. 193]).
theorem erdos_1182.variants.F_ge_pred {n : ℕ} (hn : 2 ≤ n) : n - 1 ≤ F n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 176.
Erdos1182.erdos_1182.variants.befrs_lower
Solved: stated here without proof.
Burr, Erdős, Faudree, Rousseau and Schelp [BEFRS80, Theorem 1(a)] proved
\[\frac{17n+1}{15}\leq F(n),\]the lower bound for all \(n\geq 4\).
We state the integer-part version \(n+\lfloor (2n+1)/15\rfloor\le F(n)\), which is what the proof gives (the number \(k\) of extra edges there is an integer with \(0\le k\le (2n+1)/15\)) and which follows from the printed bound because \(n+\lfloor (2n+1)/15\rfloor\leq(17n+1)/15\).
theorem erdos_1182.variants.befrs_lower {n : ℕ} (hn : 4 ≤ n) :
n + (2 * n + 1) / 15 ≤ F n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 189.
Erdos1182.erdos_1182.variants.befrs_upper
Solved: stated here without proof.
Burr, Erdős, Faudree, Rousseau and Schelp [BEFRS80, Theorem 1(b)] proved
\[F(n)\leq \left(\frac{27}{4}+o(1)\right)n(\log n)^2.\]This is superseded by the linear bounds of
erdos_1182.variants.brandtanderdos_1182.variants.nikiforov_rousseau.
theorem erdos_1182.variants.befrs_upper :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (F n : ℝ) < (27 / 4 + ε) * n * Real.log n ^ 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 200.
Erdos1182.erdos_1182.variants.brandt
Solved: stated here without proof.
The upper bound was improved to \(F(n)\leq 84n\) by Brandt [Br96]. (This resolves the final question in the negative.)
We have not seen the preprint [Br96]; the bound is as recorded on the problem page, and we state it for all large \(n\). Brandt's method uses expander graphs: almost all regular graphs of large degree are not \(3\)-good. In [BBH98, p. 6], of which Brandt is a coauthor, it is stated without proof that it gives \(F(n)<12n\) for large \(n\) (there \(F(n)\) is called \(f(K_3,n)\)).
theorem erdos_1182.variants.brandt :
∀ᶠ n : ℕ in atTop, F n ≤ 84 * n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 214.
Erdos1182.erdos_1182.variants.nikiforov_rousseau
Solved: stated here without proof.
Nikiforov and Rousseau [NiRo09, Theorem 5.1] proved that for \(n\) sufficiently large almost all connected \(100\)-regular graphs of order \(n\) are not \(3\)-good. Such a graph has \(50n\) edges (and connected \(100\)-regular graphs of order \(n\) exist for all \(n\geq 101\)), so \(F(n)<50n\) for all large \(n\). This gives a proved linear upper bound for \(F\), answering the third part.
theorem erdos_1182.variants.nikiforov_rousseau :
∀ᶠ n : ℕ in atTop, F n < 50 * n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 225.
Erdos1182.erdos_1182.variants.brandt_expects
Open: stated without proof.
Brandt [Br96] expects that for all large \(n\) we have \(2n\lt F(n)<6n\) (as recorded on the problem page).
theorem erdos_1182.variants.brandt_expects :
∀ᶠ n : ℕ in atTop, 2 * n < F n ∧ F n < 6 * n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 234.
Erdos1182.erdos_1182.variants.f_lower
Solved: stated here without proof.
Burr, Erdős, Faudree, Rousseau and Schelp [BEFRS80, Theorem 2] proved that there is a constant \(A>0\) with
\[n^{3/2}(\log n)^{1/2} \ll f(n),\]more precisely \(An^{3/2}(\log n)^{1/2}\lt f(n)\) for all sufficiently large \(n\).
theorem erdos_1182.variants.f_lower :
∃ A > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
A * (n : ℝ) ^ (3 / 2 : ℝ) * Real.sqrt (Real.log n) < (f n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 245.
Erdos1182.erdos_1182.variants.f_upper
Solved: stated here without proof.
Burr, Erdős, Faudree, Rousseau and Schelp [BEFRS80, Theorem 2] proved that there is a constant \(B>0\) with
\[f(n)\ll n^{5/3}(\log n)^{2/3},\]more precisely \(f(n)\lt Bn^{5/3}(\log n)^{2/3}\) for all sufficiently large \(n\).
theorem erdos_1182.variants.f_upper :
∃ B > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
(f n : ℝ) < B * (n : ℝ) ^ (5 / 3 : ℝ) * Real.log n ^ (2 / 3 : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 257.
Erdos1182.erdos_1182.variants.small_values
Solved: stated here without proof.
The first few values of \(F(n)\) and \(f(n)\) (beginning with \(n=2\)) are \(1,2,5,7,8\) and \(1,2,5,8,12\) respectively, as reported in [BEFRS80, Table I]. Brandt, Brinkmann and Harmuth [BBH98, Table 2] extended these (by computer) to all \(n\le 12\):
\[F(n):\ 1,2,5,7,8,11,11,16,18,23,23,\qquad f(n):\ 1,2,5,8,12,16,20,27,33,41,49\]for \(n=2,\ldots,12\). (The value for \(n=2\) is from [BEFRS80]; [BBH98] start at \(n=3\).)
theorem erdos_1182.variants.small_values :
(F 2 = 1 ∧ F 3 = 2 ∧ F 4 = 5 ∧ F 5 = 7 ∧ F 6 = 8 ∧ F 7 = 11 ∧ F 8 = 11 ∧ F 9 = 16 ∧
F 10 = 18 ∧ F 11 = 23 ∧ F 12 = 23) ∧
(f 2 = 1 ∧ f 3 = 2 ∧ f 4 = 5 ∧ f 5 = 8 ∧ f 6 = 12 ∧ f 7 = 16 ∧ f 8 = 20 ∧ f 9 = 27 ∧
f 10 = 33 ∧ f 11 = 41 ∧ f 12 = 49)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1182.lean, line 270.
Sources
TheoremErdős Problem 1183#
References: - erdosproblems.com/1183 - [Er78] Erdős, P., 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. PDF
Quoted from FormalConjectures/ErdosProblems/1183.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/1183.
The file states 4 research or textbook statements: 3 open and 1 textbook result.
Erdos1183.erdos_1183.parts.i
Open: stated without proof.
Let \(f(n)\) be maximal such that in any \(2\)-colouring of the subsets of \(\{1,\ldots,n\}\) there is always a monochromatic family of at least \(f(n)\) sets which is closed under taking unions and intersections. Estimate \(f(n)\).
Let \(F(n)\) be defined similarly, except that we only require the family be closed under taking unions. Estimate \(F(n)\). In particular, is it true that \(F(n)\geq n^{\omega(n)}\) for some \(\omega(n)\to \infty\) as \(n\to \infty\), and \(F(n)<(1+o(1))^n\)?
This is the first part, a problem of Erdős and Ulam [Er78, p. 39]. We read "estimate" as \(f(n)=\Theta(\text{answer})\).
theorem erdos_1183.parts.i :
(fun n : ℕ ↦ (f n : ℝ)) =Θ[atTop] erdos_1183.parts.i.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1183.lean, line 74.
Erdos1183.erdos_1183.parts.ii
Open: stated without proof.
Let \(f(n)\) be maximal such that in any \(2\)-colouring of the subsets of \(\{1,\ldots,n\}\) there is always a monochromatic family of at least \(f(n)\) sets which is closed under taking unions and intersections. Estimate \(f(n)\).
Let \(F(n)\) be defined similarly, except that we only require the family be closed under taking unions. Estimate \(F(n)\). In particular, is it true that \(F(n)\geq n^{\omega(n)}\) for some \(\omega(n)\to \infty\) as \(n\to \infty\), and \(F(n)<(1+o(1))^n\)?
This is the second part. We read "estimate" as \(F(n)=\Theta(\text{answer})\).
theorem erdos_1183.parts.ii :
(fun n : ℕ ↦ (F n : ℝ)) =Θ[atTop] erdos_1183.parts.ii.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1183.lean, line 92.
Erdos1183.erdos_1183.parts.iii
Open: stated without proof.
Let \(f(n)\) be maximal such that in any \(2\)-colouring of the subsets of \(\{1,\ldots,n\}\) there is always a monochromatic family of at least \(f(n)\) sets which is closed under taking unions and intersections. Estimate \(f(n)\).
Let \(F(n)\) be defined similarly, except that we only require the family be closed under taking unions. Estimate \(F(n)\). In particular, is it true that \(F(n)\geq n^{\omega(n)}\) for some \(\omega(n)\to \infty\) as \(n\to \infty\), and \(F(n)<(1+o(1))^n\)?
This is the third part, the "in particular" question: both conjuncts must hold. We state it as printed in [Er78, p. 39]: \(F(n) > n^c\) for every \(c\) if \(n > n_0(c)\), and \(F(n) < (1+\varepsilon)^n\) for every \(\varepsilon > 0\) if \(n > n_0(\varepsilon)\).
theorem erdos_1183.parts.iii :
(∀ c : ℝ, ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ c < (F n : ℝ)) ∧
∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (F n : ℝ) < (1 + ε) ^ n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1183.lean, line 110.
Erdos1183.erdos_1183.variants.f_ge
Textbook result, stated without proof.
It is trivial that \(f(n)\geq \frac{n+1}{2}\), since there is a sequence of \(n+1\) many nested subsets.
theorem erdos_1183.variants.f_ge (n : ℕ) : ((n : ℝ) + 1) / 2 ≤ (f n : ℝ)
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1183.lean, line 120.
Sources
TheoremErdős Problem 1185#
References: - erdosproblems.com/1185 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. PDF - [Fu81] Furstenberg, H., Recurrence in ergodic theory and combinatorial number theory. M. B. Porter Lectures, Princeton University Press (1981), xi+203.
Quoted from FormalConjectures/ErdosProblems/1185.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/1185.
The file states 2 research or textbook statements: 2 solved. It also has 1 API statement, counted here but not shown.
Erdos1185.erdos_1185
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1185.lean#L922.
Let \(\delta>0\) and \(k\geq 3\). Is it true that there exists \(m\geq 1\) (depending only on \(\delta\) and \(k\)) such that, for all large \(N\), if \(A,B\subseteq \{1,\ldots,N\}\) with \(\lvert A\rvert \geq \delta N\) and \(\lvert B\rvert \geq m\) then there is a non-trivial \(k\)-term arithmetic progression in \(A\) whose common difference is in \(B-B\)?
A problem of Erdős and Mauldin [Er80, p. 92], who ask the case \(k=3\) and say that the same probably holds for \(k\) terms. The answer is no, already for \(k=3\): to disprove it suffices to give an infinite set \(B\) such that \(B-B\) is not \(2\)-intersective (a set \(S\) is \(k\)-intersective if every subset of \(\mathbb{N}\) with positive density contains an arithmetic progression of length \(k+1\) whose common difference is in \(S\)), which was provided by Furstenberg [Fu81]. The statement below is the negation of the claim for all \(\delta>0\) and \(k\geq 3\), with \(m\) chosen before the threshold \(N_0\) for "large \(N\)".
theorem erdos_1185 :
¬ (∀ δ : ℝ, 0 < δ → ∀ k : ℕ, 3 ≤ k →
∃ m : ℕ, 1 ≤ m ∧ ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N →
∀ A B : Finset ℕ, A ⊆ Finset.Icc 1 N → B ⊆ Finset.Icc 1 N →
δ * (N : ℝ) ≤ (A.card : ℝ) → m ≤ B.card → HasAPWithStepInDiff k A B)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1185.lean, line 68.
Erdos1185.erdos_1185.variants.k_three
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1185.lean#L843.
The answer is already negative for \(k=3\): there is a density \(\delta>0\) such that for every \(m\geq 1\) and every \(N_0\) there are \(N\geq N_0\) and \(A,B\subseteq\{1,\ldots,N\}\) with \(\lvert A\rvert\geq\delta N\), \(\lvert B\rvert\geq m\), and no non-trivial \(3\)-term arithmetic progression in \(A\) whose common difference is in \(B-B\).
theorem erdos_1185.variants.k_three :
∃ δ : ℝ, 0 < δ ∧ ∀ m : ℕ, 1 ≤ m → ∀ N₀ : ℕ, ∃ N : ℕ, ∃ A B : Finset ℕ,
N₀ ≤ N ∧ A ⊆ Finset.Icc 1 N ∧ B ⊆ Finset.Icc 1 N ∧
δ * (N : ℝ) ≤ (A.card : ℝ) ∧ m ≤ B.card ∧ ¬ HasAPWithStepInDiff 3 A B
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1185.lean, line 84.
Sources
TheoremErdős Problem 1186#
References: - erdosproblems.com/1186 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. PDF - [PRS08] Parrilo, Pablo A. and Robertson, Aaron and Saracino, Dan, On the asymptotic minimum number of monochromatic 3-term arithmetic progressions. J. Combin. Theory Ser. A (2008), 185-192. arXiv:math/0609532
Quoted from FormalConjectures/ErdosProblems/1186.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/1186.
The file states 5 research or textbook statements: 2 open and 3 solved. It also has 1 test statement and 1 API statement, counted here but not shown.
Erdos1186.erdos_1186
Open: stated without proof.
Let \(\delta_k\) be such that in any \(2\)-colouring of \(\{1,\ldots,n\}\) there exist at least \((\delta_k+o(1))n^2\) many monochromatic \(k\)-term arithmetic progressions. Give reasonable bounds (or even an asymptotic formula) for \(\delta_k\).
We read "reasonable bounds" as determining the order of magnitude of \(\delta_k\) as \(k \to \infty\).
theorem erdos_1186 : δ =Θ[atTop] erdos_1186.answer
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1186.lean, line 92.
Erdos1186.erdos_1186.variants.van_der_waerden
Solved: stated here without proof.
Van der Waerden's theorem implies \(\delta_k\gg_k 1\).
For fixed \(k\) this says \(\delta_k > 0\).
theorem erdos_1186.variants.van_der_waerden (k : ℕ) (hk : 2 ≤ k) : 0 < δ k
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1186.lean, line 101.
Erdos1186.erdos_1186.variants.probabilistic
Solved: stated here without proof.
The probabilistic method implies
\[\delta_k \leq \frac{1}{(k-1)2^{k}}.\]
theorem erdos_1186.variants.probabilistic (k : ℕ) (hk : 2 ≤ k) :
δ k ≤ 1 / (((k : ℝ) - 1) * 2 ^ k)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1186.lean, line 109.
Erdos1186.erdos_1186.variants.prs_bounds
Solved: stated here without proof.
Parrilo, Robertson, and Saracino [PRS08] have proved
\[0.0511\approx \frac{1675}{32768}\leq \delta_3 \leq \frac{117}{2192}\approx 0.0533,\]and conjectured the upper bound is correct.
theorem erdos_1186.variants.prs_bounds : 1675 / 32768 ≤ δ 3 ∧ δ 3 ≤ 117 / 2192
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1186.lean, line 119.
Erdos1186.erdos_1186.variants.prs_conjecture
Open: stated without proof.
Parrilo, Robertson, and Saracino [PRS08] have proved
\[0.0511\approx \frac{1675}{32768}\leq \delta_3 \leq \frac{117}{2192}\approx 0.0533,\]and conjectured the upper bound is correct.
This is the conjecture \(\delta_3 = \frac{117}{2192}\).
theorem erdos_1186.variants.prs_conjecture : δ 3 = 117 / 2192
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1186.lean, line 130.
Sources
TheoremErdős Problem 1187#
References: - erdosproblems.com/1187 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [GrTa08] Green, Ben and Tao, Terence, The primes contain arbitrarily long arithmetic progressions. Ann. of Math. (2) (2008), 481-547.
Quoted from FormalConjectures/ErdosProblems/1187.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/1187.
The file states 2 research or textbook statements: 2 solved.
Erdos1187.erdos_1187.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1187.lean#L246.
Let \(k\geq 3\). Is it true that, in any finite colouring of the integers, there are monochromatic arithmetic progressions of primes of length \(k\)?
It follows from the theorem of Green and Tao [GrTa08] (that any set of primes with positive relative density contains arbitrarily long arithmetic progressions) that the answer to the first question is yes for any \(k\geq 3\).
See also 219.
theorem erdos_1187.parts.i : ∀ k : ℕ, 3 ≤ k →
∀ (κ : Type) [Finite κ] (c : ℤ → κ), ∃ S : Set ℤ, S.IsAPOfLength k ∧
(∀ n ∈ S, ∃ p : ℕ, p.Prime ∧ (p : ℤ) = n) ∧
∃ γ : κ, ∀ n ∈ S, c n = γ
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1187.lean, line 48.
Erdos1187.erdos_1187.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1187.lean#L246.
Let \(k\geq 3\). In any finite colouring of the integers, are there monochromatic arithmetic progressions of length \(k\) whose common difference is a prime?
The answer to the second question is trivially no: colouring the integers by their residue modulo \(4\) creates a colouring in which there is not even any monochromatic pair of integers whose difference is a prime. Alternatively, one can just use \(2\) colours and avoid any \(3\)-term progressions whose difference is a prime by colouring \(0,1\pmod{4}\) red and \(2,3\pmod{4}\) blue.
theorem erdos_1187.parts.ii : ¬ ∀ k : ℕ, 3 ≤ k →
∀ (κ : Type) [Finite κ] (c : ℤ → κ), ∃ (a : ℤ) (p : ℕ) (S : Set ℤ), p.Prime ∧
S.IsAPOfLengthWith k a p ∧ ∃ γ : κ, ∀ n ∈ S, c n = γ
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1187.lean, line 66.
Sources
TheoremErdős Problem 1188#
Reference: erdosproblems.com/1188
Quoted from FormalConjectures/ErdosProblems/1188.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/1188.
The file states 1 research or textbook statement: 1 solved.
Erdos1188.erdos_1188
Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-1188/Research/SparseAsymptotic.lean.
Call a set of distinct integers \(1\lt n_1\lt \cdots\lt n_k\) with associated congruence classes \(a_i\pmod{n_i}\) a distinct covering system if every integer satisfies at least one of these congruences. A minimal distinct covering system is one such that no proper subset forms a covering system. Let \(F(x)\) count the number of minimal distinct covering systems with all moduli in \([1,x]\). Estimate \(F(x)\).
The estimate is
log(log F(x)) / log x → 1.
theorem erdos_1188 :
Tendsto (fun x : ℕ => Real.log (Real.log (coveringCount x : ℝ)) / Real.log (x : ℝ))
atTop (𝓝 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1188.lean, line 76.
Sources
TheoremErdős Problem 1189#
References: - erdosproblems.com/1189 - [Er80] Erdős, P., A survey of problems in combinatorial number theory. Ann. Discrete Math. 6 (1980), 89-115. PDF - [Si85] Simpson, R. J., Regular coverings of the integers by arithmetic progressions. Acta Arith. 45 (1985), 145-152. - [Su07] Sun, Z.-W., On covering numbers. Combinatorial Number Theory, de Gruyter (2007), 443-453. arXiv:math/0601017 - [BBMST24] Balister, P., Bollobás, B., Morris, R., Sahasrabudhe, J. and Tiba, M., The structure and number of Erdős covering systems. J. Eur. Math. Soc. 26 (2024), 75-109. arXiv:1904.04806
See also erdosproblems.com/1188, which counts minimal covering systems with bounded moduli.
Quoted from FormalConjectures/ErdosProblems/1189.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/1189.
The file states 7 research or textbook statements: 3 open and 4 solved. It also has 1 test statement, counted here but not shown.
Erdos1189.erdos_1189.parts.i
Open: stated without proof.
Call a set of distinct integers \(1\lt n_1\lt \cdots\lt n_k\) a covering set if there is a choice of \(a_i\pmod{n_i}\) for \(1\leq i\leq k\) such that every integer satisfies at least one of these congruences. A set is an irreducible covering set if no proper subset is a covering set.
How many irreducible covering sets of size \(k\) are there?
This is the first part of the questions of Erdős [Er80, p. 95]. We read "how many" as asking for the asymptotics of \(\log I(k)\), where \(I(k)\) is the number of irreducible covering sets of size \(k\); this is the scale on which the number of minimal covering systems is known [BBMST24].
theorem erdos_1189.parts.i :
(fun k : ℕ ↦ Real.log (irreducibleCount k : ℝ)) ~[atTop] erdos_1189.parts.i.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1189.lean, line 93.
Erdos1189.erdos_1189.parts.ii
Open: stated without proof.
Call a set of distinct integers \(1\lt n_1\lt \cdots\lt n_k\) a covering set if there is a choice of \(a_i\pmod{n_i}\) for \(1\leq i\leq k\) such that every integer satisfies at least one of these congruences. A set is an irreducible covering set if no proper subset is a covering set.
What is the minimum and maximum that \(n_k\) can be?
This is the second part. Here \(n_k\) is the largest element of an irreducible covering set of size \(k\). The answer is a pair (minimum, maximum), stated for each \(k\) for which an irreducible covering set of size \(k\) exists.
theorem erdos_1189.parts.ii (k : ℕ)
(hk : ∃ M : Finset ℕ, IsIrreducibleCoveringSet M ∧ M.card = k) :
IsLeast (largestModulus k) (erdos_1189.parts.ii.answer k).1 ∧
IsGreatest (largestModulus k) (erdos_1189.parts.ii.answer k).2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1189.lean, line 111.
Erdos1189.erdos_1189.parts.iii
Open: stated without proof.
Call a set of distinct integers \(1\lt n_1\lt \cdots\lt n_k\) a covering set if there is a choice of \(a_i\pmod{n_i}\) for \(1\leq i\leq k\) such that every integer satisfies at least one of these congruences. A set is an irreducible covering set if no proper subset is a covering set.
Determine or estimate \(\max \sum\frac{1}{n_i}\), where the maximum ranges over all irreducible covering sets of size \(k\).
This is the third part. We read "determine or estimate" as an estimate up to constant factors. In [Er80, p. 95] the maximum is taken over the irreducible covering sets \(1\lt n_1\lt \cdots\lt n_k\leq x\), as a function of \(x\); we follow the problem page, which takes it over the irreducible covering sets of size \(k\).
theorem erdos_1189.parts.iii :
maxReciprocalSum =Θ[atTop] erdos_1189.parts.iii.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1189.lean, line 133.
Erdos1189.erdos_1189.parts.iv
Solved: stated here without proof.
Call a set of distinct integers \(1\lt n_1\lt \cdots\lt n_k\) a covering set if there is a choice of \(a_i\pmod{n_i}\) for \(1\leq i\leq k\) such that every integer satisfies at least one of these congruences. A set is an irreducible covering set if no proper subset is a covering set.
Are there infinitely many \(n\) such that the divisors of \(n\) (which are \(>1\)) form an irreducible covering set?
This is the fourth part. Sun [Su07, Theorem 1.4(i) and Corollary 1.3] proved that the answer is yes: see
erdos_1189.variants.sun.
theorem erdos_1189.parts.iv :
{n : ℕ | IsIrreducibleCoveringSet (n.divisors.filter (1 < ·))}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1189.lean, line 149.
Erdos1189.erdos_1189.variants.sun
Solved: stated here without proof.
The divisors of \(12\) (which are \(>1\)) are an example of an irreducible covering set. Sun [Su07] proved more generally that, for any odd prime \(p\), the divisors (which are \(>1\)) of \(2^{p-1}p\) form an irreducible covering set, settling the final question.
That \(n=12\) is an example is already noted in [Er80, p. 95].
theorem erdos_1189.variants.sun (p : ℕ) (hp : p.Prime) (hodd : Odd p) :
IsIrreducibleCoveringSet ((2 ^ (p - 1) * p).divisors.filter (1 < ·))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1189.lean, line 161.
Erdos1189.erdos_1189.variants.simpson
Solved: stated here without proof.
Simpson [Si85] proved \(n_k\leq 2^{k-1}\).
Here \(n_k\) is the largest element of an irreducible covering set of size \(k\). The bound follows from Simpson's theorem [Si85] (see [BBMST24, Theorem 2.4]), as stated in [BBMST24, Section 1].
theorem erdos_1189.variants.simpson (M : Finset ℕ) (hM : IsIrreducibleCoveringSet M) :
∀ n ∈ M, n ≤ 2 ^ (M.card - 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1189.lean, line 172.
Erdos1189.erdos_1189.variants.bbmst
Solved: stated here without proof.
Let \(I(k)\) count the number of irreducible covering sets of size \(k\). Balister, Bollobás, Morris, Sahasrabudhe, and Tiba [BBMST24] proved that
\[I(k) \leq \exp\left((c+o(1))\frac{k^{3/2}}{(\log k)^{1/2}}\right)\]by proving that the right-hand side is an asymptotic for the number of minimal covering systems on \(k\) moduli.
Here \(c = 4\sqrt{\tau}/3\) [BBMST24, Theorem 1.1]. The bound for \(I(k)\) follows because each irreducible covering set is the set of moduli of a minimal covering system. The \(o(1)\) is stated with an arbitrary \(\varepsilon > 0\).
theorem erdos_1189.variants.bbmst (ε : ℝ) (hε : 0 < ε) :
∀ᶠ k : ℕ in atTop, (irreducibleCount k : ℝ) ≤
Real.exp ((4 * Real.sqrt bbmstTau / 3 + ε) *
((k : ℝ) ^ (3 / 2 : ℝ) / Real.sqrt (Real.log k)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1189.lean, line 192.
Sources
TheoremErdős Problem 1190#
References: - erdosproblems.com/1190 - [BFV13] de la Bretèche, Régis and Ford, Kevin and Vandehey, Joseph, On non-intersecting arithmetic progressions. Acta Arith. (2013), 381-392. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
Quoted from FormalConjectures/ErdosProblems/1190.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/1190.
The file states 5 research or textbook statements: 5 solved.
Erdos1190.erdos_1190
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1190.lean.
Let
\[\epsilon_m=\max \sum \frac{1}{n_i}\]where the maximum is taken over all finite sequences \(m\lt n_1\lt \cdots\lt n_k\) for which there exist congruences \(a_i\pmod{n_i}\) such that no integer satisfies two such congruences.
Estimate \(\epsilon_m\).
The resolution of [202] by GPT-5.4 Pro implies via the same reduction that
\[\epsilon_m=L(m)^{-1+o(1)},\]where \(L(m)=\exp(\sqrt{\log m\log\log m})\).
theorem erdos_1190 : ∀ ε : ℝ, 0 < ε → ∀ᶠ m : ℕ in atTop,
scaleL m ^ (-1 - ε : ℝ) < eps m ∧ eps m < scaleL m ^ (-1 + ε : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1190.lean, line 63.
Erdos1190.erdos_1190.variants.lt_one
Solved: stated here without proof.
Erdős [Er80] seems to credit Mirsky and Newman with the result that \(\epsilon_m<1\), but gives no reference.
theorem erdos_1190.variants.lt_one (m : ℕ) (hm : 1 ≤ m) (S : Finset ℕ) (a : ℕ → ℤ)
(hS : ∀ n ∈ S, m < n)
(hdisj : ∀ n ∈ S, ∀ n' ∈ S, n ≠ n' → ¬ ∃ x : ℤ, x ≡ a n [ZMOD n] ∧ x ≡ a n' [ZMOD n']) :
(∑ n ∈ S, (n : ℝ)⁻¹) < 1
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1190.lean, line 72.
Erdos1190.erdos_1190.variants.tendsto_zero
Solved: stated here without proof.
He could not even decide whether \(\epsilon_m\to 0\) as \(m\to \infty\).
theorem erdos_1190.variants.tendsto_zero : Tendsto eps atTop (𝓝 0)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1190.lean, line 82.
Erdos1190.erdos_1190.variants.lower_bound
Solved: stated here without proof.
The work of de la Bretèche, Ford, and Vandehey [BFV13] implies
\[L(m)^{-1+o(1)}< \epsilon_m < L(m)^{-\sqrt{3}/2+o(1)},\]where \(L(m)=\exp(\sqrt{\log m\log\log m})\). The lower bound is implicit in their construction.
theorem erdos_1190.variants.lower_bound : ∀ ε : ℝ, 0 < ε → ∀ᶠ m : ℕ in atTop,
scaleL m ^ (-1 - ε : ℝ) < eps m
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1190.lean, line 91.
Erdos1190.erdos_1190.variants.upper_bound
Solved: stated here without proof.
The work of de la Bretèche, Ford, and Vandehey [BFV13] implies
\[L(m)^{-1+o(1)}< \epsilon_m < L(m)^{-\sqrt{3}/2+o(1)},\]where \(L(m)=\exp(\sqrt{\log m\log\log m})\). The upper bound follows immediately from their upper bound as reported in [202] and partial summation.
theorem erdos_1190.variants.upper_bound : ∀ ε : ℝ, 0 < ε → ∀ᶠ m : ℕ in atTop,
eps m < scaleL m ^ (-(sqrt 3 / 2) + ε : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1190.lean, line 102.
Sources
TheoremErdős Problem 1191#
References: - erdosproblems.com/1191 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [HaRo66] Halberstam, H. and Roth, K. F., Sequences. Vol. I. (1966), xx+291.
Quoted from FormalConjectures/ErdosProblems/1191.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/1191.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos1191.erdos_1191.parts.i
Open: stated without proof.
Let \(A\subset\mathbb{N}\) be an infinite Sidon set. Is it true that
\[\liminf_{x\to \infty} \frac{\lvert A\cap [1,x]\rvert}{x^{1/2}}(\log x)^{1/2}=0?\]Here \(x\) runs over \(\mathbb{N}\) and the \(\liminf\) is taken in
ℝ≥0∞, so that it is \(\infty\) rather than \(0\) when the sequence tends to infinity.
theorem erdos_1191.parts.i : ∀ A : Set ℕ, A.Infinite → IsSidon A →
liminf (fun x : ℕ ↦ ENNReal.ofReal
((A ∩ .Icc 1 x).ncard / (x : ℝ) ^ (1 / 2 : ℝ) * log x ^ (1 / 2 : ℝ))) atTop = 0
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1191.lean, line 44.
Erdos1191.erdos_1191.parts.ii
Open: stated without proof.
Does there exist an infinite Sidon set \(A\) such that
\[\liminf_{x\to \infty} \frac{\lvert A\cap [1,x]\rvert}{x^{1/2}}(\log x)^c>0\]for some \(c>0\)?
A positive answer would also give a positive answer to Erdős Problem 39.
theorem erdos_1191.parts.ii : ∃ A : Set ℕ, A.Infinite ∧ IsSidon A ∧
∃ c > (0 : ℝ), 0 < liminf (fun x : ℕ ↦ ENNReal.ofReal
((A ∩ .Icc 1 x).ncard / (x : ℝ) ^ (1 / 2 : ℝ) * log x ^ c)) atTop
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1191.lean, line 57.
Erdos1191.erdos_1191.variants.liminf_le
Solved: stated here without proof.
Erdős proved (see for example [HaRo66]) that if \(A\) is an infinite Sidon set then
\[\liminf_{x\to \infty} \frac{\lvert A\cap [1,x]\rvert}{x^{1/2}}(\log x)^{1/2}\leq c\]for some constant \(c>0\). See also
erdos_158.variants.isSidon'.
theorem erdos_1191.variants.liminf_le {A : Set ℕ} (hAinf : A.Infinite) (hAsid : IsSidon A) :
∃ c > (0 : ℝ), liminf (fun x : ℕ ↦ ENNReal.ofReal
((A ∩ .Icc 1 x).ncard / (x : ℝ) ^ (1 / 2 : ℝ) * log x ^ (1 / 2 : ℝ))) atTop ≤
ENNReal.ofReal c
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1191.lean, line 68.
Sources
TheoremErdős Problem 1192#
References: - erdosproblems.com/1192 - [Ru90] Ruzsa, Imre Z., A just basis. Monatsh. Math. (1990), 145--151. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. 6 (1980), 89--115.
Quoted from FormalConjectures/ErdosProblems/1192.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/1192.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 4 test statements, counted here but not shown.
Erdos1192.erdos_1192
Open: stated without proof.
Does there exist, for all \(r\geq 2\), a basis \(A\) of order \(r\) (so that \(f_r(n)>0\) for all large \(n\)) such that
\[\sum_{n\leq x}f_r(n)^2 \ll x\]for all \(x\)?
theorem erdos_1192 :
∀ r ≥ 2, ∃ A : Set ℕ,
(∀ᶠ n in atTop, f_r A r n > 0) ∧
(fun (x : ℕ) ↦ ∑ n ∈ range (x + 1), (f_r A r n : ℝ) ^ 2) =O[atTop]
(fun (x : ℕ) ↦ (x : ℝ))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1192.lean, line 97.
Erdos1192.erdos_1192.variants.renyi
Solved: stated here without proof.
Erdős and Rényi proved by the probabilistic method that there exists a set \(A\) such that
\[\sum_{n\leq x}f_r(n)^2 \ll x\]and
\[\lvert A\cap [1,x]\rvert\gg x^{1/r}\]for all \(x\).
theorem erdos_1192.variants.renyi :
∀ r ≥ 2, ∃ A : Set ℕ,
((fun (x : ℕ) ↦ ∑ n ∈ range (x + 1), (f_r A r n : ℝ) ^ 2) =O[atTop]
(fun (x : ℕ) ↦ (x : ℝ))) ∧
((fun (x : ℕ) ↦ (x : ℝ) ^ (1 / (r : ℝ))) =O[atTop]
(fun (x : ℕ) ↦ (count (· ∈ A) x : ℝ)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1192.lean, line 110.
Erdos1192.erdos_1192.variants.ruzsa
Solved: stated here without proof.
Ruzsa [Ru90] proved that the answer is yes for \(r=2\).
theorem erdos_1192.variants.ruzsa :
∃ A : Set ℕ,
(∀ᶠ n in atTop, f_r A 2 n > 0) ∧
(fun (x : ℕ) ↦ ∑ n ∈ range (x + 1), (f_r A 2 n : ℝ) ^ 2) =O[atTop]
(fun (x : ℕ) ↦ (x : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1192.lean, line 122.
Sources
TheoremErdős Problem 1193#
References: - erdosproblems.com/1193 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
Quoted from FormalConjectures/ErdosProblems/1193.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/1193.
The file states 4 research or textbook statements: 4 solved.
Erdos1193.erdos_1193.parts.i
Solved: stated here without proof.
Let \(A\subset \mathbb{N}\) and let \(g(n)\) be a non-decreasing function of \(n\) which is always \(>0\).
Is the lower density of
\[\{ n : 1_A\ast 1_A(n)=g(n)\}\]always \(0\)?
The answer is trivially no to both questions: indeed if \(A=\mathbb{N}\) (assuming \(0\in\mathbb{N}\)) then \(1_A\ast 1_A(n)=n+1\) for all \(n\). Presumably Erdős had some additional restrictions on either \(g\) or \(A\) in mind, but these are not recorded in [Er80].
theorem erdos_1193.parts.i :
¬ ∀ (A : Set ℕ) (g : ℕ → ℕ), Monotone g → (∀ n, 0 < g n) →
{n : ℕ | sumRep A n = g n}.lowerDensity = 0
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1193.lean, line 47.
Erdos1193.erdos_1193.parts.ii
Solved: stated here without proof.
Let \(A\subset \mathbb{N}\) and let \(g(n)\) be a non-decreasing function of \(n\) which is always \(>0\).
Is the upper density of
\[\{ n : 1_A\ast 1_A(n)=g(n)\}\]always \(\lt c\) for some constant \(c<1\)?
The answer is trivially no to both questions: indeed if \(A=\mathbb{N}\) (assuming \(0\in\mathbb{N}\)) then \(1_A\ast 1_A(n)=n+1\) for all \(n\). Presumably Erdős had some additional restrictions on either \(g\) or \(A\) in mind, but these are not recorded in [Er80].
theorem erdos_1193.parts.ii :
¬ ∃ c < (1 : ℝ), ∀ (A : Set ℕ) (g : ℕ → ℕ), Monotone g → (∀ n, 0 < g n) →
{n : ℕ | sumRep A n = g n}.upperDensity < c
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1193.lean, line 64.
Erdos1193.erdos_1193.variants.sumRep_univ
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1193.lean.
Indeed if \(A=\mathbb{N}\) (assuming \(0\in\mathbb{N}\)) then \(1_A\ast 1_A(n)=n+1\) for all \(n\).
theorem erdos_1193.variants.sumRep_univ (n : ℕ) : sumRep (Set.univ : Set ℕ) n = n + 1
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1193.lean, line 74.
Erdos1193.erdos_1193.variants.upper_density_pos
Solved: stated here without proof.
Erdős writes the upper density can be positive, but he believes it is bounded away from \(1\).
theorem erdos_1193.variants.upper_density_pos :
∃ (A : Set ℕ) (g : ℕ → ℕ), Monotone g ∧ (∀ n, 0 < g n) ∧
0 < {n : ℕ | sumRep A n = g n}.upperDensity
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1193.lean, line 81.
Sources
TheoremErdős Problem 1194#
References: - erdosproblems.com/1194 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. 6 (1980), 89-115. PDF - [HaRo66] Halberstam, H. and Roth, K. F., Sequences. Vol. I. Oxford University Press, Oxford (1966), xx+291. - [Le04] Lev, Vsevolod F., Reconstructing integer sets from their representation functions. Electron. J. Combin. 11 (2004), Research Paper 78, 6 pp. Link
Quoted from FormalConjectures/ErdosProblems/1194.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/1194.
The file states 4 research or textbook statements: 1 open and 3 solved. It also has 3 API statements, counted here but not shown.
Erdos1194.erdos_1194
Open: stated without proof.
Let \(A\subset\mathbb{N}\) be such that every integer \(n\geq 1\) can be written uniquely as \(a_n-b_n\) for some \(a_n,b_n\in A\). How fast must \(a_n/n\) increase?
A question of Erdős [Er80, p. 100]. Here \(a_n\) is the larger element of the representation of \(n\), not the \(n\)th element of \(A\). We read "must increase" as: the answer is the set of non-decreasing \(G\) such that every such \(A\) has \(a_n \geq c\,n\,G(n)\) for infinitely many \(n\), for some \(c>0\) depending on \(A\).
theorem erdos_1194 :
{G : ℕ → ℝ | Monotone G ∧ ∀ A : Set ℕ, IsPerfectDifferenceSetInt A →
∃ c > (0 : ℝ), HasLargeElement A (fun n ↦ c * G n * n)} = erdos_1194.answer
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1194.lean, line 100.
Erdos1194.erdos_1194.variants.exists_perfect_difference_set
Solved: stated here without proof.
Such a set is called a perfect difference set; they can be constructed, for example, by a greedy approach (as detailed by Lev [Le04]).
Erdős [Er80, p. 100] remarks that it is easy to construct such a sequence, and [Le04, Section 3] constructs a perfect difference set \(A\subseteq\mathbb{N}\) (positive integers) greedily.
theorem erdos_1194.variants.exists_perfect_difference_set :
∃ A : Set ℕ, IsPerfectDifferenceSetInt A
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1194.lean, line 113.
Erdos1194.erdos_1194.variants.greedy_upper_bound
Solved: stated here without proof.
The greedy construction achieves \(a_n\ll n^3\).
In the greedy construction of [Le04, Section 3], step \(k\) adds \(z_k\) and \(z_k+d_k\), where \(d_k\) is the least non-negative integer that is not yet a difference and \(z_k\) is the least admissible positive integer. There are \(O(k^3)\) excluded choices for \(z_k\) and \(d_k=O(k^2)\), so every element added by step \(k\) is \(O(k^3)\). As \(d_1=0\) and the \(d_k\) increase, \(n\) is represented by step \(n+1\), which gives \(a_n\ll n^3\).
theorem erdos_1194.variants.greedy_upper_bound :
∃ A : Set ℕ, IsPerfectDifferenceSetInt A ∧ ∃ C : ℝ, ∀ n : ℕ, 0 < n →
∀ a, IsLargerElement A n a → (a : ℝ) ≤ C * (n : ℝ) ^ 3
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1194.lean, line 127.
Erdos1194.erdos_1194.variants.limsup_eq_top
Solved: stated here without proof.
Erdős [Er80, p. 100] wrote it is 'easy to see' that
\[\limsup_{n\to \infty}\frac{a_n}{n}=\infty.\]Indeed, since \(A\) must be a Sidon set, if \(a_n \leq f(n)n\) for all \(n\), then all differences in \([1,x/f(x)]\) can be realised by differences from \(A\cap [1,x]\), and hence \(\lvert A\cap [1,x]\rvert^2 \gg x/f(x)\). Erdős (see for example [HaRo66]) proved that for infinitely many \(x\), \(\lvert A\cap [1,x]\rvert \ll (x/\log x)^{1/2}\), which is a contradiction for a suitable choice of \(f\).
Formally: for every perfect difference set \(A\) and every \(C\), \(a_n \geq Cn\) for infinitely many \(n\).
theorem erdos_1194.variants.limsup_eq_top :
∀ A : Set ℕ, IsPerfectDifferenceSetInt A → ∀ C : ℝ, HasLargeElement A (fun n ↦ C * n)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1194.lean, line 145.
Sources
TheoremErdős Problem 1195#
References: - erdosproblems.com/1195 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. PDF - [Ha70] Haight, J. A., A linear set of infinite measure with no two points having integral ratio. Mathematika (1970), 133--138. - [HoGPT] Ho, Boon Suan and GPT-5.4 Pro, comments on Erdős Problem 1195. erdosproblems.com forum thread. Forum - [Sc69] Schmidt, W. M., Disproof of some conjectures on Diophantine approximations. Studia Sci. Math. Hungar. (1969), 137-144. - [Sz71] Szemerédi, E., On a problem of W. Schmidt. Studia Sci. Math. Hungar. (1971), 287--288.
Quoted from FormalConjectures/ErdosProblems/1195.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/1195.
The file states 2 research or textbook statements: 2 solved.
Erdos1195.erdos_1195
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1195.lean#L1933.
Let \(S\subset \mathbb{R}\) be a set of infinite measure such that \(x/y\) is never an integer for all distinct \(x,y\in S\).
How fast can \(\lvert S\cap (0,x)\rvert\) tend to infinity?
A question of Erdős [Er80, p. 101]. Ho Boon Suan and GPT-5.4 Pro [HoGPT] settled this: if \(F:[1,\infty)\to [0,\infty)\) is a non-decreasing function tending to infinity, then there exists such a set \(S\) with \(\lvert S\cap (0,x)\rvert \geq F(x)\) if and only if
\[\int_1^\infty \frac{F(x)}{x^2}\mathrm{d}x < \infty.\]Here \(\lvert\cdot\rvert\) is Lebesgue measure, \(S\) is measurable, and the inequality is required for all sufficiently large \(x\). The statement says that the set of such \(F\) is exactly the answer.
theorem erdos_1195 :
{F : ℝ → ℝ | IsGrowthRate F ∧ HasSet F} = erdos_1195.answer
Category research solved; AMS 11 Number theory, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1195.lean, line 86.
Erdos1195.erdos_1195.variants.exists_set
Solved: stated here without proof.
Schmidt [Sc69] asked whether such a set exists. Haight [Ha70] constructed a measurable set \(E\subset(0,\infty)\) of infinite Lebesgue measure such that \(x_1/x_2\) is never an integer for distinct \(x_1,x_2\in E\), and Szemerédi [Sz71] independently constructed such a set.
theorem erdos_1195.variants.exists_set :
∃ S : Set ℝ, MeasurableSet S ∧ S ⊆ Set.Ioi 0 ∧ volume S = ⊤ ∧ IntegerRatioFree S
Category research solved; AMS 11 Number theory, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1195.lean, line 96.
Sources
TheoremErdős Problem 1196#
Reference: erdosproblems.com/1196
Quoted from FormalConjectures/ErdosProblems/1196.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/1196.
The file states 1 research or textbook statement: 1 solved.
Erdos1196.erdos_1196
Solved: stated here; a Lean proof is at https://github.com/math-inc/Erdos1196/blob/02fba13be7487cc51315f68d8fa7ef277633d3c8/PrimitiveSetsAboveX/FormalConjecturesErdos1196.lean.
Is it true that, for any \(x\), if \(A\subset [x,\infty)\) is a primitive set of integers (so that no distinct elements of \(A\) divide each other) then
\[\sum_{a\in A}\frac{1}{a\log a}< 1+o(1),\]where the \(o(1)\) term \(\to 0\) as \(x\to \infty\)?
where the \(o(1)\) term \(\to 0\) as \(x\to \infty\)?
theorem erdos_1196 :
∃ o : ℕ → ℝ, o =o[Filter.atTop] (1 : ℕ → ℝ) ∧ ∀ x > (0 : ℕ), ∀ A ⊆ Set.Ici x, IsPrimitive A →
∑' (a : A), (1 / ((a.val : ℝ).log * a)) < 1 + o x
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1196.lean, line 43.
Sources
TheoremErdős Problem 1197#
References: - erdosproblems.com/1197 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [BuMa99] Buczolich, Zoltán and Mauldin, R. Daniel, On the convergence of \(\sum^\infty_{n=1}f(nx)\) for measurable functions. Mathematika (1999), 337--341.
Quoted from FormalConjectures/ErdosProblems/1197.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/1197.
The file states 1 research or textbook statement: 1 solved.
Erdos1197.erdos_1197
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1197.lean#L705.
Let \(E\subset (0,\infty)\) be a set of positive measure. Is it true that, for almost all \(x>0\), for all sufficiently large (depending on \(x\)) integers \(n\) there exists an integer \(r\geq 1\) such that \(nx\in r\cdot E\)?
A problem of Haight, who constructed a set \(E\subset (0,\infty)\) of infinite measure such that, for all \(x\in E\), \(x\not\in r\cdot E\) if \(r\geq 2\), and also for all \(x>0\), if \(n\) is large enough then \(nx\not\in E\) (see 1195).
This is trivially true if \(E\) contains an interval \((a,b)\) with \(a\lt b\), since for any \(x>0\), for all large \(n\), the interval \((\frac{nx}{b},\frac{nx}{a})\) has length \(>1\) so contains at least one integer \(r\geq 1\).
Buczolich and Mauldin [BuMa99] proved that there exists an open set \(E\subset (0,\infty)\) and two intervals \(I,J\subset [1/2,1)\) such that, for all \(x\in I\), \(x\in \frac{1}{n}\cdot E\) for infinitely many \(n\geq 1\), and for almost all \(x\in J\), \(x\not\in \frac{1}{n}\cdot E\) for all sufficiently large (depending on \(x\)) \(n\).
This was solved in the negative by ebarschkis in the comments, who constructed a counterexample using a variant of the Buczolich-Mauldin construction.
theorem erdos_1197 : ¬ ∀ E : Set ℝ, MeasurableSet E → E ⊆ Set.Ioi 0 → 0 < volume E →
∀ᵐ x ∂(volume.restrict (Set.Ioi (0 : ℝ))), ∀ᶠ n : ℕ in atTop,
∃ r : ℕ, 1 ≤ r ∧ (n : ℝ) * x ∈ (r : ℝ) • E
Category research solved; AMS 11 Number theory, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1197.lean, line 62.
Sources
TheoremErdős Problem 1198#
References: - erdosproblems.com/1198 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [Hi74] Hindman, Neil, Finite sums from sequences within cells of a partition of \(\mathbb{N}\). J. Combinatorial Theory Ser. A (1974), 1-11. - [Sm95] Smith, Gregory L., Partitions and (\(m\) and \(n\)) sums of products. J. Combin. Theory Ser. A (1995), 77-94.
Quoted from FormalConjectures/ErdosProblems/1198.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/1198.
The file states 2 research or textbook statements: 2 solved.
Erdos1198.erdos_1198
Solved: stated here without proof.
If \(\mathbb{N}\) is \(2\)-coloured, must there exist an infinite set \(A=\{a_1\lt a_2\lt \cdots\}\) such that all expressions of the shape
\[\sum_{j=1}^{k}\prod_{i\in S_j}a_i,\]for \(k\geq 1\) and pairwise disjoint nonempty finite sets of indices \(S_1,\ldots,S_k\) (excluding the trivial expressions \(a_i\), that is \(k=1\) and \(|S_1|=1\)), have the same colour?
Erdős [Er80, p.104] wrote that "one would perhaps guess that the answer must be 'no' but no counterexample is in sight". The case where every \(S_j\) is a singleton is Hindman's theorem [Hi74]. The answer is no: a counterexample was given by Smith [Sm95].
theorem erdos_1198 :
¬ ∀ c : ℕ → Fin 2, ∃ a : ℕ → ℕ, StrictMono a ∧ 0 < a 0 ∧ ∃ col : Fin 2,
∀ (k : ℕ) (S : Fin k → Finset ℕ), 0 < k → (∀ j, (S j).Nonempty) →
Pairwise (fun j j' => Disjoint (S j) (S j')) → ¬ (k = 1 ∧ ∀ j, #(S j) = 1) →
c (∑ j, ∏ i ∈ S j, a i) = col
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1198.lean, line 51.
Erdos1198.erdos_1198.variants.hindman
Solved: stated here without proof.
The case where every \(S_j\) is a singleton (Hindman's theorem [Hi74]): for every \(2\)-colouring of \(\mathbb{N}\) there is an infinite set all of whose finite sums of distinct elements have the same colour.
theorem erdos_1198.variants.hindman :
∀ c : ℕ → Fin 2, ∃ a : ℕ → ℕ, StrictMono a ∧ 0 < a 0 ∧ ∃ col : Fin 2,
∀ T : Finset ℕ, T.Nonempty → c (∑ i ∈ T, a i) = col
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1198.lean, line 64.
Sources
TheoremErdős Problem 1199#
References: - erdosproblems.com/1199 - [Hi79] Hindman, Neil, Partitions and sums of integers with repetition. J. Combin. Theory Ser. A (1979), 19--32. - [Ow74] J. Owings, E2494. Amer. Math. Monthly (1974), 902.
Quoted from FormalConjectures/ErdosProblems/1199.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/1199.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos1199.erdos_1199
Open: stated without proof.
Is it true that in any 2-colouring of \(\mathbb{N}\) there exists an infinite set \(A\) such that all elements of \(A+A\) are the same colour?
A conjecture of Owings [Ow74].
theorem erdos_1199 :
∀ (color : ℕ → Fin 2), ∃ (A : Set ℕ),
A.Infinite ∧ ∀ n ∈ (A+A), ∀ m ∈ (A+A), color n = color m
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1199.lean, line 43.
Erdos1199.erdos_1199.variants.three
Solved: stated here; a Lean proof is at https://github.com/HowieHwong/lean-erdos-proofs/blob/b8b641ba2d00dc4d1fe205a078a4159372672459/Erdos/P1199.lean#L85.
Hindman [Hi79] has shown that this is false for 3-colourings.
theorem erdos_1199.variants.three :
∃ (color : ℕ → Fin 3), ∀ (A : Set ℕ),
A.Infinite → ∃ n ∈ (A+A), ∃ m ∈ (A+A), color n ≠ color m
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1199.lean, line 54.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.