Erdős Problem 124 to Erdős Problem 148
LemmaErdős Problem 124#
References: - erdosproblems.com/124 - [BEGL96] Burr, S. A. and Erdős, P. and Graham, R. L. and Li, W. Wen-Ching, Complete sequences of sets of integer powers. Acta Arith. (1996), 133-138.
Quoted from FormalConjectures/ErdosProblems/124.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/124.
The file states 5 research or textbook statements: 1 open and 4 solved.
Erdos124.erdos124.zero
Solved: stated here without proof.
Let \(3 \le d_1 < d_2 < \dots < d_r\) be integers such that
\[\sum_{1 \le i \le r}\frac 1{d_i - 1} \ge 1.\]Can all sufficiently large integers be written as a sum of the shape \(\sum_i c_ia_i\) where \(c_i \in \{0, 1\}\) and \(a_i\) has only the digits \(0, 1\) when written in base \(d_i\)?
Conjectured by Erdős [Er97], solved by Boris Alexeev using Aristotle.
lemma erdos124.zero :
∀ D : Finset ℕ, (∀ d ∈ D, 3 ≤ d) → 1 ≤ ∑ d ∈ D, (d - 1 : ℚ)⁻¹ →
∀ᶠ n in atTop, n ∈ ∑ d ∈ D, sumsOfDistinctPowers d 0
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/124.lean, line 48.
Erdos124.erdos124.ne_zero
Open: stated without proof.
Let \(k \ne 0\) and \(3\leq d_1 < d_2 < \cdots < d_r\) be integers of gcd equal to \(1\) such that
\[\sum_{1 \le i \le r}\frac 1{d_i - 1} \ge 1.\]Can all sufficiently large integers be written as a sum of the shape \(\sum_i c_ia_i\) where \(c_i \in \{0, 1\}\) and \(a_i\) is divisible by \(d_i ^ k\) and has only the digits \(0, 1\) when written in base \(d_i\)?
Conjectured by Burr, Erdős, Graham, and Li [BEGL96]
lemma erdos124.ne_zero :
∀ k ≠ 0, ∀ D : Finset ℕ, (∀ d ∈ D, 3 ≤ d) → 1 ≤ ∑ d ∈ D, (d - 1 : ℚ)⁻¹ → D.gcd id = 1 →
∀ᶠ n in atTop, n ∈ ∑ d ∈ D, sumsOfDistinctPowers d k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/124.lean, line 62.
Erdos124.erdos124.ne_zero_three_four_seven
Solved: stated here without proof.
All sufficiently large integers can be written as \(a + b + c\), where \(a\), \(b\), and \(c\) are divisible by \(3\), \(4\), and \(7\) respectively, and after division by that base have only the digits \(0, 1\) in that base.
Proved by Burr, Erdős, Graham, and Li [BEGL96]
lemma erdos124.ne_zero_three_four_seven :
∀ᶠ n in atTop,
n ∈ sumsOfDistinctPowers 3 1 + sumsOfDistinctPowers 4 1 + sumsOfDistinctPowers 7 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/124.lean, line 75.
Erdos124.erdos124.converse
Solved: stated here; a Lean proof is at https://github.com/arex1337/formal-conjectures-proofs/blob/3b7d581c75fd00e482deabfb20675cf3ccfaf49f/Erdos124/Converse.lean.
Let \(3\leq d_1 < d_2 < \cdots < d_r\) be integers such that all sufficiently large integers can be written as a sum of the shape \(\sum_i c_ia_i\) where \(c_i \in \{0, 1\}\) and \(a_i\) has only the digits \(0, 1\) when written in base \(d_i\). Then
\[\sum_{1 \le i \le r}\frac 1{d_i - 1} \ge 1.\]Reported by Burr, Erdős, Graham, and Li [BEGL96] as an observation of Pomerance
lemma erdos124.converse {D : Finset ℕ} (hD₃ : ∀ d ∈ D, 3 ≤ d)
(h : ∀ᶠ n in atTop, n ∈ ∑ d ∈ D, sumsOfDistinctPowers d 0) : 1 ≤ ∑ d ∈ D, (d - 1 : ℚ)⁻¹
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/124.lean, line 91.
Erdos124.erdos124.melfi_construction
Solved: stated here without proof.
For any \(\varepsilon > 0\), there exists an infinite sequence \(2 \le d_0 < d_1 < \dots\) such that the series \(\sum_{i=0}^{\infty} \frac{1}{d_i - 1}\) converges to a value at most \(\varepsilon\), and yet for every \(k \ne 0\) all sufficiently large integers can be written as \(\sum_{i \in I} a_i\) for some finite set \(I\), where each \(a_i\) is divisible by \(d_i^k\) and has only the digits \(0, 1\) when written in base \(d_i\).
The restriction \(k \ne 0\) excludes the degenerate representation of \(n\) as a sum of \(n\) copies of \(1 = d_i^0\) taken from \(n\) distinct bases.
Proved by Melfi [Me04, Proposition 1]
lemma erdos124.melfi_construction {ε : ℝ} (hε : 0 < ε) :
∃ d : ℕ → ℕ, StrictMono d ∧ 2 ≤ d 0 ∧
Summable (fun i ↦ (d i - 1 : ℝ)⁻¹) ∧ ∑' i, (d i - 1 : ℝ)⁻¹ ≤ ε ∧ ∀ k ≠ 0, ∀ᶠ n in atTop,
∃ (I : Finset ℕ) (a : ℕ → ℕ), (∀ i ∈ I, a i ∈ sumsOfDistinctPowers (d i) k) ∧
∑ i ∈ I, a i = n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/124.lean, line 108.
Sources
TheoremErdős Problem 125#
Reference: erdosproblems.com/125
There are four possibilities for the density of \(A+B\): 1. \(A+B\) has zero upper and lower density (and hence also zero density). 2. \(A+B\) has zero lower density, but positive upper density (and hence no density). 3. \(A+B\) has positive upper and lower density that are equal (and hence positive density). 4. \(A+B\) has positive upper and lower density that are unequal (and hence no density).
Quoted from FormalConjectures/ErdosProblems/125.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/125.
The file states 6 research or textbook statements: 3 open and 3 solved.
Erdos125.erdos_125
Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/300bf771bdbef43d7b9aa2521e633a50fd54dd28/FormalConjectures/ErdosProblems/125.lean.
Case 3: Does \(A + B\) have positive upper and lower density that are equal? This is the literal interpretation of "positive density" which was falsified.
theorem erdos_125 :
¬ (A + B).HasPosDensity
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/125.lean, line 67.
Erdos125.erdos_125.variants.positive_lower_density
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/c27415379b5dbe34105d1fdd707994540c4c6fc7/FormalConjectures/ErdosProblems/125.lean#L468.
Literature question: Does \(A + B\) have positive lower density?
This has been falsified.
theorem erdos_125.variants.positive_lower_density :
¬ 0 < (A + B).lowerDensity
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/125.lean, line 80.
Erdos125.erdos_125.variants.positive_upper_density
Open: stated without proof.
Literature question: Does \(A + B\) have positive upper density?
theorem erdos_125.variants.positive_upper_density :
0 < (A + B).upperDensity
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/125.lean, line 90.
Erdos125.erdos_125.variants.zero_density
Open: stated without proof.
Case 1: Does \(A + B\) have zero upper and lower density?
theorem erdos_125.variants.zero_density :
(A + B).upperDensity = 0 ∧ (A + B).lowerDensity = 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/125.lean, line 99.
Erdos125.erdos_125.variants.zero_lower_positive_upper_density
Open: stated without proof.
Case 2: Does \(A + B\) have zero lower density, but positive upper density?
theorem erdos_125.variants.zero_lower_positive_upper_density :
(A + B).lowerDensity = 0 ∧ 0 < (A + B).upperDensity
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/125.lean, line 108.
Erdos125.erdos_125.variants.positive_unequal_density
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/0bc740d2351c53713e66d9340e83f7d2c1ddecab/FormalConjectures/ErdosProblems/125.lean#L860.
Case 4: Does \(A + B\) have positive upper and lower density that are unequal?
This follows from the disproof
erdos_125.variants.positive_lower_densityabove.
theorem erdos_125.variants.positive_unequal_density :
¬ (0 < (A + B).lowerDensity ∧ (A + B).lowerDensity < (A + B).upperDensity)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/125.lean, line 121.
Sources
TheoremErdős Problem 126#
Reference: erdosproblems.com/126
Quoted from FormalConjectures/ErdosProblems/126.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/126.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos126.erdos_126
Solved: stated here; a Lean proof is at https://github.com/tadamcz/erdos126/blob/2516785fe6bbc43e979cf6029c976d9f998a7fba/Erdos126/Resolutions/Erdos126_132usd_25h.lean#L3053.
Let \(f(n)\) be maximal such that if \(A\subseteq\mathbb{N}\) has \(|A| = n\) then \(\prod_{a\neq b\in A}(a + b)\) has at least \(f(n)\) distinct prime factors. Is it true that \(\frac{f(n)}{\log n} \to\infty\)?
The answer is yes, and a machine-checked proof is available.
theorem erdos_126 : ∀ (f : ℕ → ℕ), IsMaximalAddFactorsCard f →
Tendsto (fun n => f n / Real.log n) atTop atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/126.lean, line 48.
Erdos126.erdos_126.variants.IsBigO
Solved: stated here without proof.
Erdős and Turán proved [ErTu34] in their first joint paper that
\[ \log n \ll f(n) \ll \frac{n}{\log n} \][ErTu34] Erdős, Paul and Turan, Paul, On a Problem in the Elementary Theory of Numbers. Amer. Math. Monthly (1934), 608-611.
theorem erdos_126.variants.IsBigO
(f : ℕ → ℕ)
(hf : IsMaximalAddFactorsCard f) :
((fun (n : ℕ) => Real.log n) =O[atTop] fun (n : ℕ) => (f n : ℝ)) ∧
(fun (n : ℕ) => (f n : ℝ)) =O[atTop] fun (n : ℕ) => n / Real.log n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/126.lean, line 61.
Erdos126.erdos_126.variants.isLittleO
Open: stated without proof.
Erdős says that \(f(n) = o(\frac{n}{\log n})\) has never been proved.
theorem erdos_126.variants.isLittleO
(f : ℕ → ℕ)
(hf : IsMaximalAddFactorsCard f) :
(fun (n : ℕ) => (f n : ℝ)) =o[atTop] (fun (n : ℕ) => n / Real.log n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/126.lean, line 72.
Sources
TheoremErdős Problem 127#
References: - erdosproblems.com/127 - [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231. - [Ed73] Edwards, C. S., Some extremal properties of bipartite subgraphs. Canadian J. Math. (1973), 475-485. - [Al96] Alon, Noga, Bipartite subgraphs. Combinatorica (1996), 301-311.
Quoted from FormalConjectures/ErdosProblems/127.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/127.
The file states 3 research or textbook statements: 3 solved.
Erdos127.erdos_127
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos127.lean#L585.
Let \(f(m)\) be maximal such that every graph with \(m\) edges must contain a bipartite graph with
\[\geq \frac{m}{2}+\frac{\sqrt{8m+1}-1}{8}+f(m)\]edges. Is there an infinite sequence of \(m_i\) such that \(f(m_i)\to \infty\)?
Conjectured by Erdős, Kohayakava, and Gyárfás [Er97b]. Edwards [Ed73] proved that \(f(m)\geq 0\) always. Note that \(f(\binom{n}{2})= 0\), taking \(K_n\). Solved by Alon [Al96], who showed \(f(n^2/2)\gg n^{1/2}\), and also showed that \(f(m)\ll m^{1/4}\) for all \(m\). The best possible constant in \(f(m)\leq Cm^{1/4}\) is unknown.
theorem erdos_127 : ∃ m : ℕ → ℕ, Tendsto m atTop atTop ∧
Tendsto (fun i => f (m i)) atTop atTop
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/127.lean, line 58.
Erdos127.erdos_127.variants.edwards
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos127.lean#L89.
Edwards [Ed73] proved that every graph with \(m\) edges contains a bipartite subgraph with at least \(\frac{m}{2}+\frac{\sqrt{8m+1}-1}{8}\) edges.
theorem erdos_127.variants.edwards {V : Type*} [Finite V] (G : SimpleGraph V) :
∃ H : SimpleGraph V, H ≤ G ∧ H.IsBipartite ∧
(G.edgeSet.ncard : ℝ) / 2 + (√(8 * G.edgeSet.ncard + 1) - 1) / 8 ≤ H.edgeSet.ncard
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/127.lean, line 67.
Erdos127.erdos_127.variants.alon_upper
Solved: stated here without proof.
Alon [Al96] showed that \(f(m)\ll m^{1/4}\) for all \(m\).
theorem erdos_127.variants.alon_upper : ∃ C : ℝ, ∀ m : ℕ, (f m : ℝ) ≤ C * (m : ℝ) ^ (1 / 4 : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/127.lean, line 74.
Sources
TheoremErdős Problem 128#
Reference: erdosproblems.com/128
Quoted from FormalConjectures/ErdosProblems/128.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/128.
The file states 1 research or textbook statement: 1 open.
Erdos128.erdos_128
Open: stated without proof.
Let G be a graph with n vertices such that every induced subgraph on ≥ \(n/2\) vertices has more than \(n^2/50\) edges. Must G contain a triangle?
theorem erdos_128 :
∀ (V : Type) [Fintype V] (G : SimpleGraph V),
(∀ V' : Set V, 2 * V'.ncard + 1 ≥ Fintype.card V →
50 * (G.induce V').edgeSet.ncard > Fintype.card V ^ 2) → ¬ G.CliqueFree 3
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/128.lean, line 37.
Sources
TheoremErdős Problem 130#
Reference: erdosproblems.com/130
Quoted from FormalConjectures/ErdosProblems/130.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/130.
The file states 1 research or textbook statement: 1 solved.
Erdos130.erdos_130
Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-130/Research/Basic.lean.
Let \(A\subset\mathbb{R}^2\) be an infinite set which contains no three points on a line and no four points on a circle. Consider the graph with vertices the points in \(A\), where two vertices are joined by an edge if and only if they are an integer distance apart. How large can the chromatic number and clique number of this graph be? In particular, can the chromatic number be infinite?
The chromatic number can be infinite: there is an infinite general-position set whose integer-distance graph admits no finite proper colouring. How large the clique number can be is not addressed here.
theorem erdos_130 :
∃ A : Set ℝ², A.Infinite ∧ InGeneralPosition A ∧
(IntegerDistancePlaneGraph A).chromaticNumber = ⊤
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/130.lean, line 45.
Sources
TheoremErdős Problem 131#
References: - erdosproblems.com/131 - [ELRSS99] Erdős, P. and Lev, V. and Rauzy, G. and Sándor, C. and Sárközy, A., Greedy algorithm, arithmetic progressions, subset sums and divisibility. Discrete Math. (1999), 119-135. - [PhZa24] Pham, H. T. and Zakharov, D., Sharp bound for the Erdős–Straus non-averaging set problem. arXiv:2410.14624 (2024).
Quoted from FormalConjectures/ErdosProblems/131.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/131.
The file states 3 research or textbook statements: 3 solved. It also has 5 API statements, counted here but not shown.
Erdos131.erdos_131.variants.pham_zakharov
Solved: stated here without proof.
Every non-dividing set is non-averaging. Pham and Zakharov [PhZa24] proved that a non-averaging subset of \(\{1, \dots, N\}\) has size at most \(N^{1/4 + o(1)}\), so \(F(N) \le N^{1/4 + o(1)}\).
theorem erdos_131.variants.pham_zakharov :
∃ f : ℕ → ℝ, Tendsto f atTop (𝓝 0) ∧
∀ᶠ N : ℕ in atTop, (F N : ℝ) ≤ (N : ℝ) ^ ((1 : ℝ) / 4 + f N)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/131.lean, line 93.
Erdos131.erdos_131.variants.elrss
Solved: stated here without proof.
Erdős, Lev, Rauzy, Sándor and Sárközy [ELRSS99] proved \(F(N) < 3 N^{1/2} + 1\).
theorem erdos_131.variants.elrss (N : ℕ) : (F N : ℝ) < 3 * Real.sqrt N + 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/131.lean, line 100.
Erdos131.erdos_131
Proved here.
Let \(F(N)\) be the maximal size of \(A \subseteq \{1, \dots, N\}\) such that no \(a \in A\) divides the sum of any distinct elements of \(A \setminus \{a\}\). Is it true that \(F(N) > N^{1/2 - o(1)}\)?
The answer is no, by the bound of Pham and Zakharov [PhZa24] (
erdos_131.variants.pham_zakharov).
theorem erdos_131 :
¬ ∃ f : ℕ → ℝ, Tendsto f atTop (𝓝 0) ∧
∀ᶠ N : ℕ in atTop, (N : ℝ) ^ ((1 : ℝ) / 2 - f N) < (F N : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/131.lean, line 112.
Sources
TheoremErdős Problem 133#
References: - erdosproblems.com/133 - [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231. - [HaSe84] Hanson, D. and Seyffarth, K., \(k\)-saturated graphs of prescribed maximum degree. Congr. Numer. (1984), 169-182. - [FuSe94] Füredi, Zoltán and Seress, Ákos, Maximal triangle-free graphs with restrictions on the degrees. J. Graph Theory (1994), 11-24. - [HaLe18] Haviv, Ishay and Levy, Dan, Symmetric complete sum-free sets in cyclic groups. Israel J. Math. (2018), 931-956.
Quoted from FormalConjectures/ErdosProblems/133.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/133.
The file states 6 research or textbook statements: 1 open and 5 solved.
Erdos133.erdos_133
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos133.lean#L597.
Let \(f(n)\) be minimal such that every triangle-free graph \(G\) with \(n\) vertices and diameter \(2\) contains a vertex with degree \(\geq f(n)\). What is the order of growth of \(f(n)\)? Does \(f(n)/\sqrt{n}\to \infty\)?
Asked by Erdős and Pach. The lower bound \(f(n)\geq (1-o(1))\sqrt{n}\) follows from the fact that a graph with maximum degree \(d\) and diameter \(2\) has at most \(1+d+d(d-1)=d^2+1\) many vertices.
Hanson and Seyffarth [HaSe84] proved that \(f(n)\leq (\sqrt{2}+o(1))\sqrt{n}\) using a Cayley graph on \(\mathbb{Z}/n\mathbb{Z}\), with the generating set given by some symmetric complete sum-free set of size \(\sim \sqrt{n}\). An alternative construction of such a complete sum-free set was given by Haviv and Levy [HaLe18]. Füredi and Seress [FuSe94] proved that \(f(n)\leq (\frac{2}{\sqrt{3}}+o(1))\sqrt{n}\). In particular \(f(n)/\sqrt{n}\not\to\infty\).
The precise asymptotics of \(f(n)\) are unknown; Alon believes that the truth is \(f(n)\sim \sqrt{n}\).
theorem erdos_133 : ¬ Tendsto (fun n : ℕ ↦ (f n : ℝ) / √n) atTop atTop
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/133.lean, line 68.
Erdos133.erdos_133.variants.isTheta
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos133.lean#L597.
The order of growth of \(f(n)\) is \(\sqrt{n}\).
theorem erdos_133.variants.isTheta : (fun n : ℕ ↦ (f n : ℝ)) =Θ[atTop] fun n ↦ √n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/133.lean, line 75.
Erdos133.erdos_133.variants.lower_bound
Solved: stated here without proof.
The lower bound \(f(n)\geq (1-o(1))\sqrt{n}\) follows from the fact that a graph with maximum degree \(d\) and diameter \(2\) has at most \(d^2+1\) many vertices.
theorem erdos_133.variants.lower_bound : ∀ ε : ℝ, 0 < ε →
∀ᶠ n : ℕ in atTop, (1 - ε) * √n ≤ f n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/133.lean, line 83.
Erdos133.erdos_133.variants.hanson_seyffarth
Solved: stated here without proof.
Hanson and Seyffarth [HaSe84] proved that \(f(n)\leq (\sqrt{2}+o(1))\sqrt{n}\).
theorem erdos_133.variants.hanson_seyffarth : ∀ ε : ℝ, 0 < ε →
∀ᶠ n : ℕ in atTop, (f n : ℝ) ≤ (√2 + ε) * √n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/133.lean, line 89.
Erdos133.erdos_133.variants.furedi_seress
Solved: stated here without proof.
Füredi and Seress [FuSe94] proved that \(f(n)\leq (\frac{2}{\sqrt{3}}+o(1))\sqrt{n}\).
theorem erdos_133.variants.furedi_seress : ∀ ε : ℝ, 0 < ε →
∀ᶠ n : ℕ in atTop, (f n : ℝ) ≤ (2 / √3 + ε) * √n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/133.lean, line 95.
Erdos133.erdos_133.variants.asymptotic
Open: stated without proof.
Is \(f(n)\sim \sqrt{n}\)? Alon believes that this is the truth.
theorem erdos_133.variants.asymptotic :
(fun n : ℕ ↦ (f n : ℝ)) ~[atTop] fun n ↦ √n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/133.lean, line 101.
Sources
TheoremErdős Problem 134#
References: - erdosproblems.com/134 - [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231.
Quoted from FormalConjectures/ErdosProblems/134.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/134.
The file states 1 research or textbook statement: 1 solved.
Erdos134.erdos_134
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos134.lean.
Let \(\epsilon,\delta>0\) and \(n\) be sufficiently large in terms of \(\epsilon\) and \(\delta\). Let \(G\) be a triangle-free graph on \(n\) vertices with maximum degree \(\lt n^{1/2-\epsilon}\). Can \(G\) be made into a triangle-free graph with diameter \(2\) by adding at most \(\delta n^2\) edges?
Asked by Erdős and Gyárfás, who proved that this is the case when \(G\) has maximum degree \(\ll \log n/\log\log n\). A construction of Simonovits shows that this conjecture is false if we just have maximum degree \(\leq Cn^{1/2}\), for some large enough \(C\). In this note Alon solves this problem in a strong form, in particular proving that a triangle-free graph on \(n\) vertices with maximum degree \(\lt n^{1/2-\epsilon}\) can be made into a triangle-free graph with diameter \(2\) by adding at most \(O(n^{2-\epsilon})\) edges.
theorem erdos_134 :
∀ (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ),
∃ N : ℕ, ∀ n ≥ N, ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
G.CliqueFree 3 →
(∀ v : Fin n, (G.degree v : ℝ) < Real.rpow (n : ℝ) ((1 : ℝ) / 2 - ε)) →
∃ (H : SimpleGraph (Fin n)) (_ : DecidableRel H.Adj),
G ≤ H ∧
H.CliqueFree 3 ∧
(∀ x y : Fin n, x ≠ y → H.Adj x y ∨ ∃ z, H.Adj x z ∧ H.Adj z y) ∧
((H.edgeFinset \ G.edgeFinset).card : ℝ) ≤ δ * (n : ℝ) ^ 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/134.lean, line 41.
Sources
TheoremErdős Problem 136#
References: - erdosproblems.com/136 - [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231. - [BCDP22] Bennett, P. and Cushman, R. and Dudek, A. and Pralat, P., The Erdős-Gyárfás function \(f(n,4,5)=\frac{5}{6}n+o(n)\) - so Gyárfás was right. arXiv:2207.02920 (2022). - [JoMu22] Joos, F. and Mubayi, D., Ramsey theory constructions from hypergraph matchings. arXiv:2208.12563 (2022).
Quoted from FormalConjectures/ErdosProblems/136.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/136.
The file states 1 research or textbook statement: 1 solved.
Erdos136.erdos_136
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos136.lean#L49.
Let \(f(n)\) be the smallest number of colours required to colour the edges of \(K_n\) such that every \(K_4\) contains at least \(5\) colours. Determine the size of \(f(n)\).
Asked by Erdős and Gyárfás [Er97b], who proved \(\frac56 (n - 1) < f(n) < n\) and \(f(9) = 8\); Erdős believed that the upper bound is closer to the truth. In fact \(f(n) \sim \frac56 n\), as shown by Bennett, Cushman, Dudek and Pralat [BCDP22]; Joos and Mubayi [JoMu22] found a shorter proof.
theorem erdos_136 : Tendsto (fun n : ℕ ↦ (f n : ℝ) / (n : ℝ)) atTop (𝓝 (5 / 6 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/136.lean, line 66.
Sources
TheoremErdős Problem 137#
References: - erdosproblems.com/137
Quoted from FormalConjectures/ErdosProblems/137.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/137.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos137.erdos_137
Open: stated without proof.
We say that \(N\) is powerful if whenever \(p\mid N\) we also have \(p^2\mid N\).
Let \(k\geq 3\). Can the product of any \(k\) consecutive positive integers ever be powerful?
theorem erdos_137 : ∃ k ≥ 3, ∃ n, (∏ x ∈ Finset.Ioc n (n + k), x).Powerful
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/137.lean, line 37.
Erdos137.erdos_137.variants.perfect_power
Solved: stated here without proof.
Let \(k\geq 2\). Erdős and Selfridge [ES75] proved that the product of any \(k\) consecutive integers \(N\) cannot be a perfect power.
[ES75] P. Erdös, J. L. Selfridge, "The product of consecutive integers is never a power", Illinois J. Math. 19(2): 292-301, 1975
theorem erdos_137.variants.perfect_power (k : ℕ) (hk : k ≥ 2) (n : ℕ) (x l : ℕ) (hl : 2 ≤ l) :
(∏ x ∈ Finset.Ioc n (n + k), x) ≠ x ^ l
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/137.lean, line 48.
Erdos137.erdos_137.variants.multiple_powerful_factors
Open: stated without proof.
Erdős [Er82c] conjectures that, if \(k\) is fixed, then for all \(n\) sufficiently large and all positive integers \(m\), there must be at least \(k\) distinct primes \(p\) such that \(p\mid m(m+1)\cdots (m+n)\) and yet \(p^2\) does not divide the right hand side.
[Er82c] Erdős, Paul, "Miscellaneous problems in number theory". Congr. Numer. (1982), 25-45.,
theorem erdos_137.variants.multiple_powerful_factors (k : ℕ) : ∀ᶠ n in Filter.atTop,
∀ (m : ℕ) (hm : 0 < m),
letI N := ∏ x ∈ Finset.Ioc m (m + n), x
∃ P : Finset ℕ, P.card = k ∧ ∀ p ∈ P, p.Prime ∧
p ∣ N ∧ ¬ p ^ 2 ∣ N
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/137.lean, line 60.
Sources
TheoremErdős Problem 138#
References: - erdosproblems.com/138 - [Be68] Berlekamp, E. R., A construction for partitions which avoid long arithmetic progressions. Canad. Math. Bull. (1968), 409-414. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [Go01] Gowers, W. T., A new proof of Szemerédi's theorem. Geom. Funct. Anal. (2001), 465-588. - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al. - [CFS26] Campos, M., Fox, J. and Schildkraut, C., A new lower bound for two-color van der Waerden numbers. arXiv:2608.20824 (2026). - [OAI26] OpenAI, Quantitative Superexponential Bounds for van der Waerden Numbers. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026/paper.pdf
Quoted from FormalConjectures/ErdosProblems/138.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/138.
The file states 7 research or textbook statements: 1 open and 6 solved. It also has 2 test statements, counted here but not shown.
Erdos138.monoAP_guarantee_set_nonempty
Solved: stated here without proof.
Asserts that for any number of colors
rand any progression lengthk, there always exists some numberNlarge enough to guarantee a monochromatic arithmetic progression. In other words, the setmonoAP_guarantee_setis non-empty. This is the fundamental existence result that allows for the definition of the van der Waerden numbers.
theorem monoAP_guarantee_set_nonempty (r k) : (monoAP_guarantee_set r k).Nonempty
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/138.lean, line 62.
Erdos138.erdos_138
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/ProgressionColoring/Main.lean#L12.
In [Er80] Erdős asks whether
\[ \lim_{k \to \infty} (W(k))^{1/k} = \infty \]Yes. This was proved by an internal OpenAI model in September 2026 [OAI26], which shows \(W(k) > k^{k/100000}\) for all large \(k\); see the linked Lean proof.
theorem erdos_138 : atTop.Tendsto (fun k => (W k : ℝ)^(1/(k : ℝ))) atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/138.lean, line 99.
Erdos138.erdos_138.variants.prime
Solved: stated here without proof.
When \(p\) is prime Berlekamp [Be68] has proved \(W(p+1) ≥ p^{2^p}\).
theorem erdos_138.variants.prime (p : ℕ) (hp : p.Prime) : p * (2 ^ p) ≤ W (p + 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/138.lean, line 107.
Erdos138.erdos_138.variants.upper
Solved: stated here without proof.
Gowers [Go01] has proved
\[W(k) \leq 2^{2^{2^{2^{2^{k+9}}}}.\]
theorem erdos_138.variants.upper (k : ℕ) : W k ≤ 2 ^ (2 ^ (2 ^ 2 ^ 2 ^ (k + 9)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/138.lean, line 114.
Erdos138.erdos_138.variants.quotient
Open: stated without proof.
In [Er81] Erdős asks whether \(\frac{W(k+1)}{W(k)} \to \infty\).
theorem erdos_138.variants.quotient :
atTop.Tendsto (fun k => ((W (k + 1) : ℚ)/(W k))) atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/138.lean, line 121.
Erdos138.erdos_138.variants.difference
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/6ac8d0cbe1a85e71747c62c1391a84788015ebc1/FormalConjectures/ErdosProblems/138.lean#L844.
In [Er81] Erdős asks whether \(W(k+1) - W(k) \to \infty\).
The DeepMind prover agent has found a formal proof of this statement.
theorem erdos_138.variants.difference :
atTop.Tendsto (fun k => (W (k + 1) - W k)) atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/138.lean, line 133.
Erdos138.erdos_138.variants.dvd_two_pow
Solved: stated here; a Lean proof is at https://github.com/niketp03/atlas-fc-verified/blob/15e4b3a7584e218cec531aeaf71cce72a8a9ecb1/AtlasFCSolutions/Erdos138.lean#L1033.
In [Er80] Erdős asks whether \(W(k)/2^k\to \infty\).
Campos, Fox and Schildkraut [CFS26] independently prove \(W(k) \geq (1 - o(1)) k 2^{k-1}\), which implies this; they report that their proof was generated with ChatGPT. (The related variant
erdos_138.variants.difference, \(W(k+1) - W(k) \to \infty\), was solved separately in [arxiv/2605.22763].)Solved: a Lean 4 proof, derived from the Atlas proofs in facebookresearch/atlas-lean, is linked in
formal_proof.
theorem erdos_138.variants.dvd_two_pow :
atTop.Tendsto (fun k => ((W k : ℚ)/ (2 ^ k))) atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/138.lean, line 153.
Sources
TheoremErdős Problem 139#
Reference: erdosproblems.com/139
Quoted from FormalConjectures/ErdosProblems/139.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/139.
The file states 1 research or textbook statement: 1 solved.
Erdos139.erdos_139
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos139.lean#L36.
Erdős Problem 139: Let \(r_k(N)\) be the size of the largest subset of \({1,...,N}\) which does not contain a non-trivial \(k\)-term arithmetic progression. Prove that \(r_k(N) = o(N)\).
theorem erdos_139 (k : ℕ) (hk : 1 < k) :
Filter.Tendsto (fun N => (r k N / N : ℝ)) Filter.atTop (𝓝 0)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/139.lean, line 43.
Sources
TheoremErdős Problem 141#
References: - erdosproblems.com/141 - Wikipedia
Quoted from FormalConjectures/ErdosProblems/141.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/141.
The file states 5 research or textbook statements: 4 open and 1 solved. It also has 2 test statements, counted here but not shown.
Erdos141.erdos_141
Open: stated without proof.
Let \(k≥3\). Are there \(k\) consecutive primes in arithmetic progression?
theorem erdos_141 :
∀ k ≥ 3, ∃ (s : Set ℕ), s.IsAPAndPrimeProgressionOfLength k
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/141.lean, line 78.
Erdos141.erdos_141.variants.first_cases
Solved: stated here without proof.
The existence of such progressions has been verified for \(k≤10\).
theorem erdos_141.variants.first_cases :
(∀ k ≥ 3, k ≤ 10 → ∃ (s : Set ℕ), s.IsAPAndPrimeProgressionOfLength k)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/141.lean, line 86.
Erdos141.erdos_141.variants.eleven
Open: stated without proof.
Are there \(11\) consecutive primes in arithmetic progression?
theorem erdos_141.variants.eleven :
∃ (s : Set ℕ), s.IsAPAndPrimeProgressionOfLength 11
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/141.lean, line 94.
Erdos141.erdos_141.variants.infinite_three
Open: stated without proof.
It is open, even for \(k=3\), whether there are infinitely many such progressions.
theorem erdos_141.variants.infinite_three :
(consecutivePrimeArithmeticProgressions 3).Infinite
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/141.lean, line 108.
Erdos141.erdos_141.variants.infinite_general_case
Open: stated without proof.
Fix a \(k \geq 3\). Is it true that there are infinitely many arithmetic prime progressions of length \(k\)?
theorem erdos_141.variants.infinite_general_case :
∀ k ≥ 3, (consecutivePrimeArithmeticProgressions k).Infinite
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/141.lean, line 116.
Sources
TheoremErdős Problem 142#
Reference: erdosproblems.com/142
Quoted from FormalConjectures/ErdosProblems/142.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/142.
The file states 4 research or textbook statements: 4 open.
Erdos142.erdos_142
Open: stated without proof.
Prove an asymptotic formula for \(r_k(N)\), the largest possible size of a subset of \(\{1, \dots, N\}\) that does not contain any non-trivial \(k\)-term arithmetic progression. That is, find \(f_k\) with \(r_k(N) / f_k(N) \to 1\) as \(N \to \infty\).
theorem erdos_142 (k : ℕ) : (fun N => (r k N : ℝ)) ~[atTop] erdos_142.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/142.lean, line 42.
Erdos142.erdos_142.variants.lower
Open: stated without proof.
Show that \(r_k(N) = o_k(N / \log N)\), where \(r_k(N)\) the largest possible size of a subset of \(\{1, \dots, N\}\) that does not contain any non-trivial \(k\)-term arithmetic progression.
theorem erdos_142.variants.lower (k : ℕ) (hk : 1 < k) :
(fun N => (r k N : ℝ)) =o[atTop] (fun N : ℕ => N / (N : ℝ).log)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/142.lean, line 50.
Erdos142.erdos_142.variants.isTheta
Open: stated without proof.
Determine the order of magnitude of \(r_k(N)\), the largest possible size of a subset of \(\{1, \dots, N\}\) that does not contain any non-trivial \(k\)-term arithmetic progression. That is, find \(f_k\) with \(r_k(N) \asymp_k f_k(N)\).
theorem erdos_142.variants.isTheta (k : ℕ) :
(fun N => (r k N : ℝ)) =Θ[atTop] erdos_142.variants.isTheta.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/142.lean, line 63.
Erdos142.erdos_142.variants.three
Open: stated without proof.
Prove an asymptotic formula for \(r_3(N)\), the largest possible size of a subset of \(\{1, \dots, N\}\) that does not contain any non-trivial \(3\)-term arithmetic progression. That is, find \(f\) with \(r_3(N) / f(N) \to 1\) as \(N \to \infty\).
theorem erdos_142.variants.three : (fun N => (r 3 N : ℝ)) ~[atTop] erdos_142.variants.three.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/142.lean, line 78.
Sources
TheoremErdős Problem 143#
Reference: erdosproblems.com/143
Quoted from FormalConjectures/ErdosProblems/143.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/143.
The file states 2 research or textbook statements: 2 open.
Erdos143.erdos_143.parts.i
Open: stated without proof.
Does this imply that
\[ \liminf \frac{|A \cap [1,x]|}{x} = 0? \]
theorem erdos_143.parts.i : ∀ (A : Set ℝ), WellSeparatedSet A →
liminf (fun x => (A ∩ (Set.Icc 1 x)).ncard / x) atTop = 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/143.lean, line 48.
Erdos143.erdos_143.parts.ii
Open: stated without proof.
Or
\[ \sum_{x \in A} \frac{1}{x \log x} < \infty, \]
theorem erdos_143.parts.ii (A : Set ℝ) (h : WellSeparatedSet A) :
Summable fun (x : A) ↦ 1 / (x * Real.log x)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/143.lean, line 59.
Sources
TheoremErdős Problem 145#
Reference: erdosproblems.com/145
Quoted from FormalConjectures/ErdosProblems/145.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/145.
The file states 4 research or textbook statements: 1 open and 3 solved.
Erdos145.erdos_145
Open: stated without proof.
Let \(s_1 < s_2 < \cdots\) be the sequence of squarefree numbers. Is it true that, for any \(\alpha\geq 0\),
\[ \lim_{x\to\infty} \frac{1}{x}\sum_{s_n\leq x}(s_{n+1}-s_n)^\alpha \]exists?
theorem erdos_145 :
∀ α ≥ (0 : ℝ), ∃ β : ℝ,
atTop.Tendsto (fun x : ℝ ↦ 1 / x * ∑ n ∈ A x, (s (n + 1) - s n : ℝ) ^ α) (𝓝 β)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/145.lean, line 49.
Erdos145.erdos_145.variants.le_two
Solved: stated here without proof.
Erdős [Er51] proved this for all \(0\leq \alpha\leq 2\).
[Er51] Erdös, P., Some problems and results in elementary number theory. Publ. Math. Debrecen (1951), 103-109.
theorem erdos_145.variants.le_two {α : ℝ} (hα : α ∈ Set.Icc 0 2) :
∃ β : ℝ,
atTop.Tendsto (fun x : ℝ ↦ 1 / x * ∑ n ∈ A x, (s (n + 1) - s n : ℝ) ^ α) (𝓝 β)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/145.lean, line 61.
Erdos145.erdos_145.variants.le_three
Solved: stated here without proof.
Hooley [Ho73] extended this to all \(0 \leq \alpha\leq 3\).
[Ho73] Hooley, Christopher, On the intervals between consecutive terms of sequences. Proc. Symp. Pure Math, vol. 24, pp. 129-140. 1973.
theorem erdos_145.variants.le_three {α : ℝ} (hα : α ∈ Set.Icc 0 3) :
∃ β : ℝ,
atTop.Tendsto (fun x : ℝ ↦ 1 / x * ∑ n ∈ A x, (s (n + 1) - s n : ℝ) ^ α) (𝓝 β)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/145.lean, line 72.
Erdos145.erdos_145.variants.lt_eleven_thirds
Solved: stated here without proof.
Greaves, Harman, and Huxley showed (in Chapter 11 of [GHH97]) that this is true for \(0 \leq \alpha < 11/3\).
[GHH97] Greaves, G. R. H. and Harman, G. and Huxley, M. N., Sieve Methods, Exponential Sums, and their Applications in Number Theory. (1997).
theorem erdos_145.variants.lt_eleven_thirds {α : ℝ} (hα : α ∈ Set.Ico 0 (11 / 3)) :
∃ β : ℝ,
atTop.Tendsto (fun x : ℝ ↦ 1 / x * ∑ n ∈ A x, (s (n + 1) - s n : ℝ) ^ α) (𝓝 β)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/145.lean, line 85.
Sources
TheoremErdős Problem 146#
References: - erdosproblems.com/146 - [ErSi84] Erdős, P. and Simonovits, M., Cube-supersaturated graphs and related problems. Progress in graph theory (1984), 203-218. - [OpenAI26] OpenAI, Ten advances in mathematics and theoretical computer science. (2026).
Quoted from FormalConjectures/ErdosProblems/146.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/146.
The file states 2 research or textbook statements: 2 solved.
Erdos146.erdos_146
Solved: stated here without proof.
If \(H\) is bipartite and is \(r\)-degenerate, that is, every induced subgraph of \(H\) has minimum degree \(\leq r\), then
\[\mathrm{ex}(n;H) \ll n^{2-1/r}.\]The answer is no. OpenAI [OpenAI26] give a connected bipartite
2-degenerateHand constantsc, ε > 0with \(\mathrm{ex}(n;H)\geq cn^{3/2+\epsilon}\) for all largen, which exceeds the conjectured \(n^{2-1/2}=n^{3/2}\). Seeerdos_146.variants.two_degenerate_counterexample.
theorem erdos_146 :
¬ ∀ (r q : ℕ) (H : SimpleGraph (Fin q)),
0 < r → H.IsBipartite → H.IsDegenerate r →
Asymptotics.IsBigO atTop
(fun n : ℕ => (extremalNumber n H : ℝ))
(fun n : ℕ => (n : ℝ) ^ ((2 : ℝ) - 1 / (r : ℝ)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/146.lean, line 46.
Erdos146.erdos_146.variants.two_degenerate_counterexample
Solved: stated here; a Lean proof is at https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6/CompactnessAndDegeneracy.lean.
The counterexample: a connected bipartite
2-degenerateHwhose extremal number exceeds \(n^{3/2+\epsilon}\) infinitely often, so ther = 2case oferdos_146fails.
theorem erdos_146.variants.two_degenerate_counterexample :
∃ (q : ℕ) (H : SimpleGraph (Fin q)),
H.Connected ∧ H.IsBipartite ∧ H.IsDegenerate 2 ∧
∃ c ε : ℝ, 0 < c ∧ 0 < ε ∧
∀ᶠ n : ℕ in atTop,
c * (n : ℝ) ^ ((3 : ℝ) / 2 + ε) ≤ (extremalNumber n H : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/146.lean, line 61.
Sources
TheoremErdős Problem 147#
References: - erdosproblems.com/147 - [ErSi84] Erdős, P. and Simonovits, M., Cube-supersaturated graphs and related problems. Progress in graph theory (Waterloo, Ont., 1982) (1984), 203-218. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [Ja23] Janzer, Oliver, Rainbow Turán number of even cycles, repeated patterns and blow-ups of cycles. Israel J. Math. (2023), 813--840. - [Ja23b] Janzer, Oliver, Disproof of a conjecture of Erdős and Simonovits on the Turán number of graphs with minimum degree 3. Int. Math. Res. Not. IMRN (2023), 8478--8494.
Quoted from FormalConjectures/ErdosProblems/147.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/147.
The file states 4 research or textbook statements: 1 open and 3 solved.
Erdos147.erdos_147
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos147.lean#L799.
If \(H\) is bipartite with minimum degree \(r\) then there exists \(\epsilon=\epsilon(H)>0\) such that
\[\mathrm{ex}(n;H) \gg n^{2-\frac{1}{r-1}+\epsilon}.\]Conjectured by Erdős and Simonovits [ErSi84]. A probabilistic argument shows that there exists some \(\epsilon=\epsilon(H)>0\) such that \(\mathrm{ex}(n;H) \gg n^{2-\frac{2}{r}+\epsilon}\).
This conjecture was disproved by Janzer [Ja23] for even \(r\geq 4\). The case \(r=3\) was disproved by Janzer [Ja23b], who constructed, for any \(\epsilon>0\), a \(3\)-regular bipartite graph \(H\) such that \(\mathrm{ex}(n;H)\ll n^{\frac{4}{3}+\epsilon}\).
In [Ja23] Janzer conjectures that the above lower bound is sharp, in that for any \(r\geq 3\) and \(\epsilon>0\) there exists an \(r\)-regular graph \(H\) such that \(\mathrm{ex}(n;H) \ll n^{2-\frac{2}{r}+\epsilon}\). Janzer's result proves this for even \(r\geq 4\).
The conjecture is stated for minimum degree \(r \geq 2\) (for \(r = 1\) the exponent \(2 - \frac{1}{r-1}\) is not meaningful).
theorem erdos_147 :
¬ ∀ (V : Type) [Fintype V] [Nonempty V] (H : SimpleGraph V) [DecidableRel H.Adj],
H.IsBipartite → 2 ≤ H.minDegree → ∃ ε : ℝ, 0 < ε ∧
(fun n : ℕ => (n : ℝ) ^ (2 - 1 / ((H.minDegree : ℝ) - 1) + ε)) =O[atTop]
fun n : ℕ => (extremalNumber n H : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/147.lean, line 68.
Erdos147.erdos_147.variants.janzer_even
Solved: stated here without proof.
Janzer [Ja23] disproved the conjecture for even \(r\geq 4\): for any even \(r \geq 4\) and \(\epsilon>0\) there exists a nonempty \(r\)-regular bipartite graph \(H\) such that \(\mathrm{ex}(n;H) \ll n^{2-\frac{2}{r}+\epsilon}\).
theorem erdos_147.variants.janzer_even (r : ℕ) (hr : 4 ≤ r) (heven : Even r) (ε : ℝ)
(hε : 0 < ε) :
∃ (q : ℕ) (H : SimpleGraph (Fin q)), 0 < q ∧ H.IsBipartite ∧ H.IsRegularOfDegree r ∧
(fun n : ℕ => (extremalNumber n H : ℝ)) =O[atTop]
fun n : ℕ => (n : ℝ) ^ (2 - 2 / (r : ℝ) + ε)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/147.lean, line 82.
Erdos147.erdos_147.variants.cubic
Solved: stated here without proof.
Janzer [Ja23b] constructed, for any \(\epsilon>0\), a nonempty \(3\)-regular bipartite graph \(H\) such that \(\mathrm{ex}(n;H)\ll n^{\frac{4}{3}+\epsilon}\).
theorem erdos_147.variants.cubic (ε : ℝ) (hε : 0 < ε) :
∃ (q : ℕ) (H : SimpleGraph (Fin q)), 0 < q ∧ H.IsBipartite ∧ H.IsRegularOfDegree 3 ∧
(fun n : ℕ => (extremalNumber n H : ℝ)) =O[atTop]
fun n : ℕ => (n : ℝ) ^ (4 / 3 + ε : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/147.lean, line 95.
Erdos147.erdos_147.variants.janzer_conjecture
Open: stated without proof.
Janzer [Ja23] conjectures that for any \(r\geq 3\) and \(\epsilon>0\) there exists a nonempty \(r\)-regular graph \(H\) such that \(\mathrm{ex}(n;H) \ll n^{2-\frac{2}{r}+\epsilon}\).
theorem erdos_147.variants.janzer_conjecture : ∀ r : ℕ, 3 ≤ r → ∀ ε : ℝ, 0 < ε →
∃ (q : ℕ) (H : SimpleGraph (Fin q)), 0 < q ∧ H.IsRegularOfDegree r ∧
(fun n : ℕ => (extremalNumber n H : ℝ)) =O[atTop]
fun n : ℕ => (n : ℝ) ^ (2 - 2 / (r : ℝ) + ε)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/147.lean, line 107.
Sources
TheoremErdős Problem 148#
References: - erdosproblems.com/148 - [ElPl21] Elsholtz, Christian and Planitzer, Stefan, Sums of four and more unit fractions and approximate parametrizations. Bull. Lond. Math. Soc. (2021), 695-709. - [Ko14] Konyagin, S. V., Double exponential lower bound for the number of representations of unity by Egyptian fractions. Math. Notes (2014), 277-281. - OEIS A006585
Quoted from FormalConjectures/ErdosProblems/148.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/148.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 5 test statements, counted here but not shown.
Erdos148.erdos_148
Open: stated without proof.
Let \(F(k)\) be the number of solutions to
\[ 1= \frac{1}{n_1}+\cdots+\frac{1}{n_k},\]where \(1\leq n_1\lt \cdots\lt n_k\) are distinct integers. Find good estimates for \(F(k)\).
theorem erdos_148 : (fun k ↦ (F k : ℝ)) =Θ[atTop] erdos_148.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/148.lean, line 174.
Erdos148.erdos_148.variants.lower_bound
Solved: stated here without proof.
The current best bounds known are
\[2^{c^{\frac{k}{\log k}}}\leq F(k) \leq c_0^{(\frac{1}{5}+o(1))2^k},\]where \(c>0\) is some absolute constant and \(c_0=1.5979102\ldots\) is the square of the 'Vardi constant' \(1.26408\cdots\). The lower bound is due to Konyagin [Ko14] and the upper bound to Elsholtz and Planitzer [ElPl21]. (erdosproblems.com gives \(c_0=1.26408\cdots\); [ElPl21, Remark 3] gives \(c_0=1.5979102\ldots\).)
[Ko14, Theorem 1] states the lower bound in the explicit form
\[F(k) \geq \exp\left(\exp\left(\left(\frac{(\log 2)(\log 3)}{3}+o(1)\right) \frac{k}{\log k}\right)\right) \quad (k \to \infty),\]which is the statement formalised here.
theorem erdos_148.variants.lower_bound :
∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ᶠ k : ℕ in atTop,
exp (exp ((log 2 * log 3 / 3 + o k) * ((k : ℝ) / log k))) ≤ F k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/148.lean, line 191.
Erdos148.erdos_148.variants.upper_bound
Solved: stated here without proof.
The current best bounds known are
\[2^{c^{\frac{k}{\log k}}}\leq F(k) \leq c_0^{(\frac{1}{5}+o(1))2^k},\]where \(c>0\) is some absolute constant and \(c_0=1.5979102\ldots\) is the square of the 'Vardi constant' \(1.26408\cdots\). The lower bound is due to Konyagin [Ko14] and the upper bound to Elsholtz and Planitzer [ElPl21]. (erdosproblems.com gives \(c_0=1.26408\cdots\); [ElPl21, Remark 3] gives \(c_0=1.5979102\ldots\).)
[ElPl21, Corollary 3(2)] shows that for every \(\varepsilon > 0\) and all \(k \geq k(\varepsilon)\), the number \(f_k(1,1) \geq F(k)\) of solutions with \(n_1 \leq \cdots \leq n_k\) is less than \(c_0^{(\frac{2}{5}+\varepsilon)2^{k-1}} = c_0^{(\frac{1}{5}+\frac{\varepsilon}{2})2^k}\).
theorem erdos_148.variants.upper_bound :
∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ᶠ k : ℕ in atTop,
(F k : ℝ) ≤ c₀ ^ ((1 / 5 + o k) * 2 ^ k)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/148.lean, line 209.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.