Erdős Problem 291 to Erdős Problem 299
TheoremErdős Problem 291#
References: - erdosproblems.com/291 - [ErGr80, p.34] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Sh16] P. Shiu, The denominators of harmonic numbers. arXiv:1607.02863 (2016). - [WuYa22] Wu, Bing-Ling and Yan, Xiao-Hui, On the denominators of harmonic numbers. {IV}. C. R. Math. Acad. Sci. Paris (2022), 53--57.
Quoted from FormalConjectures/ErdosProblems/291.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/291.
The file states 6 research or textbook statements: 3 open and 3 solved. It also has 2 test statements, counted here but not shown.
Erdos291.erdos_291.parts.i
Open: stated without proof.
Let \(n\geq 1\) and define \(L_n\) to be the least common multiple of \(\{1,\ldots,n\}\) and \(a_n\) by \(\sum_{1\leq k\leq n}\frac{1}{k}=\frac{a_n}{L_n}\).
Is it true that \((a_n,L_n)=1\) occurs for infinitely many \(n\)?
theorem erdos_291.parts.i :
{ n : ℕ | Nat.gcd (a n) (L n) = 1 }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/291.lean, line 63.
Erdos291.erdos_291.parts.ii
Solved: stated here without proof.
Is it true that \((a_n,L_n)>1\) occurs for infinitely many \(n\)?
Steinerberger has observed that the answer to the second question is trivially yes: for example, any \(n\) which begins with a \(2\) in base \(3\) has \(3\mid (a_n,L_n)\).
theorem erdos_291.parts.ii :
{ n : ℕ | Nat.gcd (a n) (L n) > 1 }.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/291.lean, line 74.
Erdos291.erdos_291.variants.steinerberger_generalization
Solved: stated here without proof.
More generally, if the leading digit of \(n\) in base \(p\) is \(p-1\) then \(p\mid (a_n,L_n)\). There is in fact a necessary and sufficient condition: a prime \(p\leq n\) divides \((a_n,L_n)\) if and only if \(p\) divides the numerator of \(1+\cdots+\frac{1}{k}\), where \(k\) is the leading digit of \(n\) in base \(p\). This can be seen by writing \(a_n = \frac{L_n}{1}+\cdots+\frac{L_n}{n}\) and observing that the right-hand side is congruent to \(1+\cdots+1/k\) modulo \(p\). (The previous claim about \(p-1\) follows immediately from Wolstenholme's theorem.)
theorem erdos_291.variants.steinerberger_generalization (n p : ℕ) (hp : p.Prime) (hpn : p ≤ n) :
let k := n / p ^ Nat.log p n;
p ∣ Nat.gcd (a n) (L n) ↔ (p : ℤ) ∣ (∑ i ∈ Finset.Icc 1 k, (1 : ℚ) / i).num
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/291.lean, line 87.
Erdos291.erdos_291.variants.shiu_heuristic_asymptotic
Open: stated without proof.
This leads to a heuristic prediction (see for example a preprint of Shiu [Sh16]) of \(\asymp\frac{x}{\log x}\) for the number of \(n\in [1,x]\) such that \((a_n,L_n)=1\).
theorem erdos_291.variants.shiu_heuristic_asymptotic :
Asymptotics.IsTheta atTop
(fun x : ℕ ↦ ((((Finset.Icc 1 x).filter (fun n ↦ Nat.gcd (a n) (L n) = 1)).card : ℝ)))
(fun x : ℕ ↦ (x : ℝ) / Real.log x)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/291.lean, line 97.
Erdos291.erdos_291.variants.shiu_heuristic_density_zero
Open: stated without proof.
In particular, there should be infinitely many \(n\), but the set of such \(n\) should have density zero. Unfortunately this heuristic is difficult to turn into a proof.
theorem erdos_291.variants.shiu_heuristic_density_zero :
Filter.Tendsto (fun N : ℕ ↦
((((Finset.Icc 1 N).filter (fun n ↦ Nat.gcd (a n) (L n) = 1)).card : ℝ) / (N : ℝ)))
atTop (nhds 0)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/291.lean, line 108.
Erdos291.erdos_291.variants.wu_yan
Solved: stated here without proof.
Wu and Yan [WuYa22] have proved, conditional on \(\frac{1}{\log p}\) being linearly independent over \(\mathbb{Q}\) for any finite collection of primes \(p\) (itself a consequence of Schanuel's conjecture), that the set of \(n\) for which \((a_n,L_n)>1\) has upper density \(1\).
theorem erdos_291.variants.wu_yan
(h_indep : LinearIndependent ℚ (fun p : {p : ℕ // p.Prime} ↦ 1 / Real.log (p : ℝ))) :
atTop.limsup (fun N : ℕ ↦
((((Finset.Icc 1 N).filter (fun n ↦ Nat.gcd (a n) (L n) > 1)).card : ℝ) /
(N : ℝ) : EReal)) = 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/291.lean, line 120.
Sources
TheoremErdős Problem 292#
References: - erdosproblems.com/292 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Ma00] Martin, Greg, Denser Egyptian fractions. Acta Arith. (2000), 231-260.
Quoted from FormalConjectures/ErdosProblems/292.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/292.
The file states 5 research or textbook statements: 5 solved.
Erdos292.erdos_292
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos292.lean#L116.
Let \(A\) be the set of \(n\in \mathbb{N}\) such that there exist \(1\leq m_1\lt \cdots \lt m_k=n\) with \(\sum\tfrac{1}{m_i}=1\). Explore \(A\). In particular, does \(A\) have density \(1\)?
Straus observed that \(A\) is closed under multiplication. Furthermore, it is easy to see that \(A\) does not contain any prime power.
The answer is yes, as proved by Martin [Ma00], who in fact proved that if \(B=\mathbb{N}\backslash A\) then, for all large \(x\),
\[\frac{\lvert B\cap [1,x]\rvert}{x}\asymp \frac{\log\log x}{\log x},\]and also gave an essentially complete description of \(B\) as those integers which are small multiples of prime powers.
van Doorn has observed that if \(n\in A\) (with \(n>1\)) then \(2n\in A\) also, since if \(\sum \frac{1}{m_i}=1\) then \(\frac{1}{2}+\sum\frac{1}{2m_i}=1\) also.
theorem erdos_292 : A.HasDensity 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/292.lean, line 60.
Erdos292.erdos_292.variants.martin
Solved: stated here without proof.
Martin [Ma00] proved that if \(B=\mathbb{N}\backslash A\) then \(\frac{\lvert B\cap [1,x]\rvert}{x}\asymp \frac{\log\log x}{\log x}\).
theorem erdos_292.variants.martin :
(fun x : ℕ ↦ ((Aᶜ ∩ Set.Icc 1 x).ncard : ℝ) / x) =Θ[atTop]
fun x ↦ Real.log (Real.log x) / Real.log x
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/292.lean, line 66.
Erdos292.erdos_292.variants.mul
Solved: stated here without proof.
Straus observed that \(A\) is closed under multiplication.
theorem erdos_292.variants.mul : ∀ m ∈ A, ∀ n ∈ A, m * n ∈ A
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/292.lean, line 73.
Erdos292.erdos_292.variants.prime_pow
Solved: stated here without proof.
\(A\) does not contain any prime power.
theorem erdos_292.variants.prime_pow : ∀ n ∈ A, ¬ IsPrimePow n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/292.lean, line 78.
Erdos292.erdos_292.variants.two_mul
Solved: stated here without proof.
van Doorn observed that if \(n\in A\) (with \(n>1\)) then \(2n\in A\) also.
theorem erdos_292.variants.two_mul : ∀ n ∈ A, 1 < n → 2 * n ∈ A
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/292.lean, line 83.
Sources
TheoremErdős Problem 294#
References: - erdosproblems.com/294 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [LiSa24] Liu, Y. and Sawhney, M., On further questions regarding unit fractions. arXiv:2404.07113 (2024).
Quoted from FormalConjectures/ErdosProblems/294.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/294.
The file states 2 research or textbook statements: 2 solved. It also has 2 API statements, counted here but not shown.
Erdos294.erdos_294
Solved: stated here without proof.
Let \(N\geq 1\) and let \(t(N)\) be the least integer \(t\) such that there is no solution to
\[1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}\]with \(t=n_1\lt \cdots \lt n_k\leq N\). Estimate \(t(N)\).
Solved by Liu and Sawhney [LiSa24, Theorem 1.6] (up to \((\log\log N)^{O(1)}\)), who proved that
\[\frac{N}{(\log N)(\log\log N)^3(\log\log\log N)^{O(1)}}\ll t(N) \ll \frac{N}{\log N}.\]The unspecified \(O(1)\) exponent is the real number
K.
theorem erdos_294 :
(∃ K : ℝ, (fun N : ℕ => (N : ℝ) / (Real.log N * Real.log (Real.log N) ^ 3 *
Real.log (Real.log (Real.log N)) ^ K)) ≪ (fun N : ℕ => (t N : ℝ))) ∧
((fun N : ℕ => (t N : ℝ)) ≪ (fun N : ℕ => (N : ℝ) / Real.log N))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/294.lean, line 71.
Erdos294.erdos_294.variants.erdos_graham_upper
Solved: stated here without proof.
Erdős and Graham [ErGr80, p. 35] could show that \(t(N)\ll\frac{N}{\log N}\). They gave no proof; one is in [LiSa24, Section 4].
theorem erdos_294.variants.erdos_graham_upper :
(fun N : ℕ => (t N : ℝ)) ≪ (fun N : ℕ => (N : ℝ) / Real.log N)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/294.lean, line 82.
Sources
LemmaErdős Problem 295#
Reference: erdosproblems.com/295
Quoted from FormalConjectures/ErdosProblems/295.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/295.
The file states 3 research or textbook statements: 1 open, 1 solved and 1 textbook result.
Erdos295.exists_k
Textbook result, stated without proof.
Helper lemma: for each \(N\), there exists \(k\) and \(n_1 < ... < n_k\) such that \(N ≤ n_1 < ⋯ < n_k\) with \(\frac 1 {n_1} + ... + \frac 1 {n_k} = 1\).
lemma exists_k (N : ℕ) : ∃ (k : ℕ) (n : Fin k → ℕ),
(∀ i, N ≤ n i) ∧ StrictMono n ∧ ∑ i, (1 / n i : ℝ) = 1
Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/295.lean, line 37.
Erdos295.erdos_295
Open: stated without proof.
Let \(k(N)\) denote the smallest \(k\) such that there exists \(N ≤ n_1 < ⋯ < n_k\) with \(\frac 1 {n_1} + ... + \frac 1 {n_k} = 1\)
Is it true that \(\lim_{N \to \infty} k(N) - (e - 1)N = \infty\)?
theorem erdos_295 :
Filter.atTop.Tendsto (fun N => k N - (rexp 1 - 1)*N) Filter.atTop
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/295.lean, line 58.
Erdos295.erdos_295.variants.erdos_straus
Solved: stated here without proof.
Erdős and Straus have proved the existence of some constant \(c>0\) such that \(-c < k(N)-(e-1)N \ll \frac N {\log N}\)
theorem erdos_295.variants.erdos_straus :
∃ᵉ (C > 0) (O > 0), ∀ᶠ (N : ℕ) in Filter.atTop,
(k N - (rexp 1 - 1)*N) ∈ Set.Ioc (-C) (O * N / (N : ℝ).log)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/295.lean, line 67.
Sources
TheoremErdős Problem 296#
References: - erdosproblems.com/296 - [Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021).
Quoted from FormalConjectures/ErdosProblems/296.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/296.
The file states 1 research or textbook statement: 1 solved.
Erdos296.erdos_296
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos296.lean.
Let \(N\geq 1\) and let \(k(N)\) be maximal such that there are \(k\) disjoint \(A_1,\ldots,A_k\subseteq \{1,\ldots,N\}\) with \(\sum_{n\in A_i}\frac{1}{n}=1\) for all \(i\). Estimate \(k(N)\). Is it true that \(k(N)=o(\log N)\)?
Hunter and Sawhney observed that Bloom's theorem [Bl21], together with the greedy argument, gives \(k(N)=(1-o(1))\log N\).
theorem erdos_296 :
(∀ N k : ℕ, HasDisjointUnitDecomps N k → (k : ℚ) ≤ recipSum (Finset.Icc 1 N)) ∧
(∀ ε : ℝ, 0 < ε → ε < 1 → ∀ᶠ N : ℕ in atTop,
HasDisjointUnitDecomps N ⌊(1 - ε) * Real.log N⌋₊)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/296.lean, line 55.
Sources
TheoremErdős Problem 298#
References: - erdosproblems.com/298 - [Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021).
Quoted from FormalConjectures/ErdosProblems/298.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/298.
The file states 2 research or textbook statements: 2 solved.
Erdos298.erdos_298
Solved: stated here; a proof in another system is at https://github.com/b-mehta/unit-fractions/blob/master/src/final_results.lean.
Does every set \(A \subseteq \mathbb{N}\) of positive density contain some finite \(S \subset A\) such that \(\sum_{n \in S} \frac{1}{n} = 1\)?
The answer is yes, proved by Bloom [Bl21] (even if 'positive density' is interpreted as 'positive upper density', which is likely what Erdős intended).
The theorem below uses the positive-upper-density interpretation; the literal natural-density interpretation is recorded separately.
This was formalized in Lean 3 by Bloom and Mehta.
theorem erdos_298 : (∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity →
∃ (S : Finset ℕ), ↑S ⊆ A ∧ ∑ n ∈ S, (1 / n : ℚ) = 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/298.lean, line 46.
Erdos298.erdos_298.variants.natural_density
Solved: stated here without proof.
The literal natural-density interpretation of Erdős Problem 298 follows from [Bl21].
theorem erdos_298.variants.natural_density : (∀ (A : Set ℕ), 0 ∉ A →
A.HasPosDensity →
∃ (S : Finset ℕ), ↑S ⊆ A ∧ ∑ n ∈ S, (1 / n : ℚ) = 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/298.lean, line 54.
Sources
TheoremErdős Problem 299#
References: - erdosproblems.com/298 - erdosproblems.com/299 - [Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021).
Quoted from FormalConjectures/ErdosProblems/299.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/299.
The file states 2 research or textbook statements: 2 solved.
Erdos299.erdos_299
Solved: stated here; a proof in another system is at https://github.com/b-mehta/unit-fractions/blob/master/src/final_results.lean.
Is there an infinite sequence \(a_1 < a_2 < \dots\) such that \(a_{i+1} - a_i = O(1)\) and no finite sum of \(\frac{1}{a_i}\) is equal to 1?
There does not exist such a sequence, which follows from the positive solution to [erdosproblems.com/298] by Bloom [Bl21].
This was formalized in Lean 3 by Bloom and Mehta.
theorem erdos_299 : ¬ (∃ (a : ℕ → ℕ),
StrictMono a ∧ (∀ n, 0 < a n) ∧
(fun n ↦ (a (n + 1) : ℝ) - a n) =O[atTop] (1 : ℕ → ℝ) ∧
∀ S : Finset ℕ, ∑ i ∈ S, (1 : ℝ) / a i ≠ 1)
Category research solved; AMS 11 Number theory, 40 Sequences, series, summability. Declared in FormalConjectures/ErdosProblems/299.lean, line 46.
Erdos299.erdos_299.variants.density
Solved: stated here without proof.
The corresponding question is also false if one replaces sequences such that \(a_{i+1} - a_i = O(1)\) with sets of positive density, as follows from [Bl21].
The statement is as follows: If \(A \subset \mathbb{N}\) has positive upper density (and hence certainly if \(A\) has positive density) then there is a finite \(S \subset A\) such that \(\sum_{n \in S} \frac{1}{n} = 1\).
theorem erdos_299.variants.density : ∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity →
∃ S : Finset ℕ, ↑S ⊆ A ∧ ∑ n ∈ S, (1 : ℝ) / n = 1
Category research solved; AMS 11 Number theory, 40 Sequences, series, summability. Declared in FormalConjectures/ErdosProblems/299.lean, line 61.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.