Erdős Problem 1095 to Erdős Problem 1099
TheoremErdős Problem 1095#
References: - erdosproblems.com/1095 - [EES74] Ecklund, Jr., E. F. and Erd\H{o}s, P. and Selfridge, J. L., A new function associated with the prime factors of {\((\sp{n}\sb{k})\)}. Math. Comp. (1974), 647--649. - [ELS93] Erdős, P. and Lacampagne, C. B. and Selfridge, J. L., Estimates of the least prime factor of a binomial coefficient. Math. Comp. (1993), 215--224. - [GrRa96] Granville, Andrew and Ramaré, Olivier, Explicit bounds on exponential sums and the scarcity of squarefree binomial coefficients. Mathematika (1996), 73--107. - [Ko99b] Konyagin, S. V., Estimates of the least prime factor of a binomial coefficient. Mathematika (1999), 41--55. - [SSW20] Sorenson, Brianna and Sorenson, Jonathan and Webster, Jonathan, An algorithm and estimates for the {E}rdős-{S}elfridge function. (2020), 371--385.
Quoted from FormalConjectures/ErdosProblems/1095.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/1095.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos1095.erdos_1095.variants.lower_solved
Solved: stated here without proof.
The current record is \(g(k) \gg \exp(c(\log k)^2)\) for some \(c>0\), due to Konyagin [Ko99b]. -
theorem erdos_1095.variants.lower_solved :
∃ c > 0, (fun k : ℕ ↦ exp (c * log k ^ 2)) =O[atTop] fun k ↦ (g k : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1095.lean, line 54.
Erdos1095.erdos_1095.variants.upper_conjecture
Solved: stated here without proof.
Ecklund, Erdős, and Selfridge [EES74] proved \(g(k)\leq \exp((1+o(1))k)\).
theorem erdos_1095.variants.upper_conjecture :
∃ f : ℕ → ℝ, Tendsto f atTop (𝓝 0) ∧ ∀ᶠ k in atTop, g k ≤ exp (k * (1 + f k))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1095.lean, line 62.
Erdos1095.erdos_1095.variants.lower_conjecture
Open: stated without proof.
Erdős, Lacampagne, and Selfridge [ELS93] write 'it is clear to every right-thinking person' that \(g(k)\geq\exp(c\frac{k}{\log k})\) for some constant \(c>0\).
theorem erdos_1095.variants.lower_conjecture : ∃ c > 0, ∀ᶠ k in atTop, g k ≥ exp (c * k / log k)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1095.lean, line 71.
Erdos1095.erdos_1095.variants.log_equivalent
Open: stated without proof.
Sorenson, Sorenson, and Webster [SSWE20] give heuristic evidence that \(\log g(k) \asymp \frac{k}{\log k}\).
theorem erdos_1095.variants.log_equivalent :
(fun k ↦ log (g k)) =Θ[atTop] (fun k ↦ (k : ℝ) / log k)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1095.lean, line 78.
Sources
TheoremErdős Problem 1096#
References: - erdosproblems.com/1096 - [ErKo98] Erdős, P. and Komornik, V., Developments in non-integer bases. Acta Math. Hungar. (1998), 57--83. - [Fe16] Feng, D.-J., On the topology of polynomials with bounded integer coefficients. J. Eur. Math. Soc. (2016), 181--193.
Quoted from FormalConjectures/ErdosProblems/1096.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/1096.
The file states 1 research or textbook statement: 1 solved.
Erdos1096.erdos_1096
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/dfe2d78128b493c572cf525b1b8edf4897fb7664/src/latest/ErdosProblems/Erdos1096.lean#L44.
Let \(1\lt q<1+\epsilon\) and consider the set of numbers of the shape \(\sum_{i\in S}q^i\) (for all finite \(S\)), ordered by size as \(0=x_1\lt x_2\lt \cdots\).
Is it true that, provided \(\epsilon>0\) is sufficiently small, \(x_{k+1}-x_k \to 0\)?
This was solved affirmatively by Erdős and Komornik [ErKo98], who proved the conclusion whenever \(1\lt q\lt \sqrt{q_1}\), where \(q_1\) is the second Pisot-Vijayaraghavan number.
theorem erdos_1096 :
∃ ε > 0, ∀ q, 1 < q → q < 1 + ε →
∀ x : ℕ → ℝ, StrictMono x → Set.range x = { ∑ i ∈ S, q ^ i | S : Finset ℕ } →
Tendsto (fun k => x (k + 1) - x k) atTop (𝓝 0)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1096.lean, line 51.
Sources
TheoremErdős Problem 1097#
References: - erdosproblems.com/1097 - [Bo99] Bourgain, J., On the dimension of {K}akeya sets and related maximal inequalities. Geom. Funct. Anal. (1999), 256--282 - [KaTa99] Katz, Nets Hawk and Tao, Terence, Bounds on arithmetic projections, and applications to the {K}akeya conjecture. Math. Res. Lett. (1999), 625--630. - [Le15] Lemm, Marius, New counterexamples for sums-differences. Proc. Amer. Math. Soc. (2015), 3863--3868. - [GGTW25] B. Georgiev, J. Gómez-Serrano, T. Tao, and A. Wagner, Mathematical exploration and discovery at scale. arXiv:2511.02864 (2025).
Quoted from FormalConjectures/ErdosProblems/1097.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/1097.
The file states 3 research or textbook statements: 1 solved and 2 textbook results.
Erdos1097.erdos_1097
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/f13dd54b520cdf2136fdd3a04f0f9fa50e311358/FormalConjectures/ErdosProblems/1097.lean#L306.
The main conjecture: for any finite set of integers \(A\) with \(|A| = n\), the number of distinct common differences in three-term arithmetic progressions is \(O(n^{3/2})\).
This conjecture was resolved negatively by showing that the problem is exactly equivalent to Bourgain's sums-differences question [Bo99], which was introduced as an arithmetic path towards the Kakeya conjecture. Under this equivalence: - The greatest achievable exponent for this problem is equal to the smallest constant \(c\) achievable for Bourgain's sums-differences question:
\[|A -_G B| \ll \max(|A|, |B|, |A +_G B|)^c\]
- The \(O(n^{3/2})\) prediction is disproved because the lower bound has been shown to satisfy \(c \ge 1.77898\) (due to Zheng and AlphaEvolve [GGTW25], improving on Lemm [Le15]), which is strictly greater than \(3/2 = 1.5\).
- The best known upper bound is \(c \le 11/6 \approx 1.833\) (due to Katz and Tao [KaTa99]).
- While the specific \(O(n^{3/2})\) prediction is resolved negatively, the general question of determining the exact optimal exponent \(c\) remains open.
theorem erdos_1097 : ¬ ∃ C > (0 : ℝ), ∀ (A : Finset ℤ),
(CommonDifferencesThreeTermAP A).ncard ≤ C * (A.card : ℝ) ^ (3 / 2 : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1097.lean, line 66.
Erdos1097.erdos_1097.variants.weaker
Textbook result, proved here.
A weaker bound has been proven: there are always at most \(n^2\) such values of \(d\).
theorem erdos_1097.variants.weaker :
∀ A, (CommonDifferencesThreeTermAP A).ncard ≤ A.card ^ 2
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1097.lean, line 74.
Erdos1097.erdos_1097.variants.lower_bound
Textbook result, proved here.
A trivial lower bound: for sufficiently large
nthere exist sets \(A\) with \(|A| = n\) that contain at least \(\Omega(n)\) distinct common differences of three-term arithmetic progressions.
theorem erdos_1097.variants.lower_bound : ∃ c > (0 : ℝ), ∀ᶠ n in Filter.atTop, ∃ (A : Finset ℤ),
A.card = n ∧ c * (n : ℝ) ≤ (CommonDifferencesThreeTermAP A).ncard
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1097.lean, line 94.
Sources
TheoremErdős Problem 1098#
References: - erdosproblems.com/1098 - [Ne76] Neumann, B. H., A problem of Paul Erdős on groups. J. Austral. Math. Soc. Ser. A (1976), 467-472.
Quoted from FormalConjectures/ErdosProblems/1098.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/1098.
The file states 3 research or textbook statements: 3 solved. It also has 1 API statement, counted here but not shown.
Erdos1098.erdos_1098
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1098.lean.
Let \(G\) be a group and \(\Gamma=\Gamma(G)\) be the non-commuting graph, with vertices the elements of \(G\) and an edge between \(g\) and \(h\) if and only if \(g\) and \(h\) do not commute, \(gh\neq hg\).
If \(\Gamma\) contains no infinite complete subgraph, then is there a finite bound on the size of complete subgraphs of \(\Gamma\)?
This was solved by Neumann [Ne76], who proved that \(\Gamma\) contains no infinite complete subgraph if and only if the centre of the group has finite index, and noted that if the centre has index \(n\) then \(\Gamma\) contains no complete subgraph on \(>n\) vertices.
theorem erdos_1098 :
∀ (G : Type*) [Group G],
(∀ s : Set G, (nonCommutingGraph G).IsClique s → s.Finite) →
∃ n : ℕ, ∀ s : Finset G, (nonCommutingGraph G).IsClique (s : Set G) → s.card ≤ n
Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1098.lean, line 56.
Erdos1098.erdos_1098.variants.center_finiteIndex
Solved: stated here without proof.
Neumann [Ne76] proved that \(\Gamma\) contains no infinite complete subgraph if and only if the centre of the group has finite index.
theorem erdos_1098.variants.center_finiteIndex (G : Type*) [Group G] :
(∀ s : Set G, (nonCommutingGraph G).IsClique s → s.Finite) ↔
(Subgroup.center G).FiniteIndex
Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1098.lean, line 67.
Erdos1098.erdos_1098.variants.upper_bound
Solved: stated here without proof.
Neumann [Ne76] noted that if the centre has index \(n\) then \(\Gamma\) contains no complete subgraph on \(>n\) vertices.
theorem erdos_1098.variants.upper_bound (G : Type*) [Group G]
[(Subgroup.center G).FiniteIndex] :
(nonCommutingGraph G).CliqueFree ((Subgroup.center G).index + 1)
Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1098.lean, line 77.
Sources
TheoremErdős Problem 1099#
References: - erdosproblems.com/1099 - [Er81h] Erdős, P., Some problems and results on additive and multiplicative number theory. Analytic number theory (Philadelphia, Pa., 1980) (1981), 171-182. - [Vo84] Vose, Michael D., Integers with consecutive divisors in small ratio. J. Number Theory (1984), 233-238. - [Te87] Tenenbaum, Gérald, Sur un problème extrémal en arithmétique. Ann. Inst. Fourier (1987), 1-18.
Quoted from FormalConjectures/ErdosProblems/1099.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/1099.
The file states 4 research or textbook statements: 4 solved.
Erdos1099.erdos_1099
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1099.lean#L63.
Let \(1=d_1\lt \cdots\lt d_{\tau(n)}=n\) be the divisors of \(n\), and for \(\alpha>1\) let
\[h_\alpha(n) = \sum_i \left( \frac{d_{i+1}}{d_i}-1\right)^\alpha.\]Is it true that
\[\liminf_{n\to \infty}h_\alpha(n) \ll_\alpha 1?\]Erdős [Er81h] remarks that \(n!\) or the least common multiple of \(\{1,\ldots,n\}\) would be good candidates for an infinite sequence of \(n\) with \(h_\alpha(n)\) bounded.
The \(\liminf\) is trivially \(\geq 1\), just considering the term \(i=1\). A positive answer to the main question was provided by Vose [Vo84] by constructing a specific sequence. Tenenbaum [Te87] proved that the two explicit sequences mentioned above satisfy this property.
The statement "\(\liminf h_\alpha(n)\) is finite" is formalised as "\(h_\alpha(n)\leq C\) for infinitely many \(n\)".
theorem erdos_1099 :
∀ α : ℝ, 1 < α → ∃ C : ℝ, ∃ᶠ n : ℕ in atTop, h α n ≤ C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1099.lean, line 66.
Erdos1099.erdos_1099.variants.factorial
Solved: stated here without proof.
Is \(h_\alpha(n!)\) bounded? Tenenbaum [Te87, Théorème 1] proved that it is, for every \(\alpha > 1\).
theorem erdos_1099.variants.factorial : ∀ α : ℝ, 1 < α →
∃ C : ℝ, ∀ n : ℕ, h α n.factorial ≤ C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1099.lean, line 73.
Erdos1099.erdos_1099.variants.lcm
Solved: stated here without proof.
Is \(h_\alpha(\mathrm{lcm}(1,\ldots,n))\) bounded? Tenenbaum [Te87, Théorème 1] proved that it is, for every \(\alpha > 1\).
theorem erdos_1099.variants.lcm : ∀ α : ℝ, 1 < α →
∃ C : ℝ, ∀ n : ℕ, h α ((Finset.Icc 1 n).lcm id) ≤ C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1099.lean, line 80.
Erdos1099.erdos_1099.variants.ratio_sum
Solved: stated here without proof.
Erdős remarks that this problem occurred to him when considering \(\sum_i \frac{d_{i+1}}{d_i}\). It is easy to see that \(\sum_{i} \frac{d_{i+1}}{d_i}> \tau(n)+\log n\), and Erdős asked whether
\[\liminf \left(\sum_{i} \frac{d_{i+1}}{d_i}-\tau(n)-\log n\right)\lt \infty,\]which follows from the affirmative answer to the main question.
theorem erdos_1099.variants.ratio_sum : ∃ C : ℝ, ∃ᶠ n : ℕ in atTop,
∑ i : Fin (n.divisors.card - 1), ((Nat.nth (· ∣ n) (i + 1) : ℝ) / Nat.nth (· ∣ n) i) -
n.divisors.card - Real.log n ≤ C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1099.lean, line 91.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.