Erdős Problem 445 to Erdős Problem 470
TheoremErdős Problem 445#
References: - erdosproblems.com/445 - [He00] Heath-Brown, D. R., Arithmetic applications of {K}loosterman sums. Nieuw Arch. Wiskd. (5) (2000), 380--384. - MathOverflow
Quoted from FormalConjectures/ErdosProblems/445.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/445.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.
Erdos445.erdos_445
Open: stated without proof.
Is it true that, for any \(c>1/2\), if \(p\) is a sufficiently large prime then, for any \(n\geq 0\), there exist \(a,b\in(n,n+p^c)\) such that \(ab\equiv 1\pmod{p}\)?
This is discussed in this MathOverflow question [MathOverflow].
theorem erdos_445 :
∀ c : ℝ, c > 1 / 2 →
∀ᶠ p : ℕ in atTop, p.Prime → ∀ n : ℕ, Erdos445Prop c p n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/445.lean, line 53.
Erdos445.erdos_445.variants.heilbronn
Solved: stated here without proof.
Heilbronn (unpublished) proved this for \(c\) sufficiently close to \(1\).
theorem erdos_445.variants.heilbronn :
∃ c₀ < 1, ∀ c : ℝ, c > c₀ →
∀ᶠ p : ℕ in atTop, p.Prime → ∀ n : ℕ, Erdos445Prop c p n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/445.lean, line 62.
Erdos445.erdos_445.variants.heath_brown
Solved: stated here without proof.
Heath-Brown [He00] used Kloosterman sums to prove this for all \(c>3/4\).
theorem erdos_445.variants.heath_brown :
∀ c : ℝ, c > 3 / 4 →
∀ᶠ p : ℕ in atTop, p.Prime → ∀ n : ℕ, Erdos445Prop c p n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/445.lean, line 71.
Sources
TheoremErdős Problem 447#
References: - erdosproblems.com/447 - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [Kl71] Kleitman, Daniel, Collections of subsets containing no two sets and their union. Proceedings of the LA Meeting AMS (1971), 153-155.
Quoted from FormalConjectures/ErdosProblems/447.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/447.
The file states 2 research or textbook statements: 2 solved.
Erdos447.erdos_447.parts.i
Solved: stated here without proof.
How large can a union-free collection \(\mathcal{F}\) of subsets of \([n]\) be? By union-free we mean there are no solutions to \(A\cup B=C\) with distinct \(A,B,C\in \mathcal{F}\). Must \(\lvert \mathcal{F}\rvert =o(2^n)\)?
In [Er65b] Erdős reported that the estimate \(\lvert \mathcal{F}\rvert=o(2^n)\) was proved in unpublished work by Sárközy and Szemerédi.
theorem erdos_447.parts.i :
(fun n : ℕ => (maxUnionFree n : ℝ)) =o[atTop] (fun n : ℕ => (2 : ℝ) ^ n)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/447.lean, line 50.
Erdos447.erdos_447.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos447.lean.
How large can a union-free collection \(\mathcal{F}\) of subsets of \([n]\) be? By union-free we mean there are no solutions to \(A\cup B=C\) with distinct \(A,B,C\in \mathcal{F}\). Perhaps even
\[\lvert \mathcal{F}\rvert <(1+o(1))\binom{n}{\lfloor n/2\rfloor}?\]Solved by Kleitman [Kl71], who proved
\[\lvert \mathcal{F}\rvert <(1+o(1))\binom{n}{\lfloor n/2\rfloor}.\]
theorem erdos_447.parts.ii :
∃ c : ℕ → ℝ, (c =o[atTop] (1 : ℕ → ℝ)) ∧ ∀ᶠ n : ℕ in atTop,
(maxUnionFree n : ℝ) < (1 + c n) * (n.choose (n / 2) : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/447.lean, line 64.
Sources
TheoremErdős Problem 448#
References: - erdosproblems.com/448 - OEIS A397433: the integer sequence \(\tau^+(n)\) (the constant \(\alpha\) in Ford's asymptotic is OEIS A074738). - [Er79] Erdős, Paul, Some unconventional problems in number theory. Math. Mag. (1979), 67-70. - [Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73-82. - [HaTe88] Hall, Richard R. and Tenenbaum, Gérald, Divisors. (1988), xvi+167. - [ErTe81] Erdős, P., Tenenbaum, G., Sur la structure de la suite des diviseurs d'un entier. Ann. Inst. Fourier (Grenoble) 31 (1981), 17–37. - [Fo08] Ford, Kevin, The distribution of integers with a divisor in a given interval. Ann. of Math. (2) 168 (2008), 367–433. - [Te13] Tenenbaum, Gérald, Some of Erdős' unconventional problems in number theory, thirty-four years later. Erdős Centennial, Bolyai Soc. Math. Stud. 25 (2013), 651–681.
Quoted from FormalConjectures/ErdosProblems/448.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/448.
The file states 5 research or textbook statements: 5 solved. It also has 3 test statements, counted here but not shown.
Erdos448.erdos_448
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos448.lean#L35.
Let \(\tau(n)\) count the divisors of \(n\) and \(\tau^+(n)\) count the number of \(k\) such that \(n\) has a divisor in \([2^k, 2^{k+1})\). Is it true that, for all \(\epsilon > 0\),
\[ \tau^+(n) < \epsilon \cdot \tau(n) \]for almost all \(n\)?
This is false, and was disproved by Erdős and Tenenbaum [ErTe81], who showed that in fact the upper density of the set of such \(n\) is \(\asymp \epsilon^{1-o(1)}\) (where the \(o(1)\) in the exponent \(\to 0\) as \(\epsilon \to 0\)). A more precise result was proved by Hall and Tenenbaum [HaTe88] (see Section 4.6), who showed that the upper density is \(\ll \epsilon \log(2/\epsilon)\). Hall and Tenenbaum further prove that \(\tau^+(n)/\tau(n)\) has a distribution function. Erdős and Graham also asked whether there is a good inequality known for \(\sum_{n \leq x} \tau^+(n)\). This was provided by Ford [Fo08] who proved
\[ \sum_{n \leq x} \tau^+(n) \asymp x\frac{(\log x)^{1-\alpha}}{(\log\log x)^{3/2}} \]where
\[ \alpha = 1-\frac{1+\log\log 2}{\log 2} = 0.08607\cdots. \]
theorem erdos_448 :
¬ ∀ ε : ℝ, 0 < ε →
{n : ℕ | (tauPlus n : ℝ) < ε * (n.divisors.card : ℝ)}.HasDensity 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/448.lean, line 86.
Erdos448.erdos_448.variants.erdos_tenenbaum
Solved: stated here without proof.
Quantitative form of the (negative) answer to
erdos_448. Erdős and Tenenbaum [ErTe81] showed that the upper density of \(\{n : \tau^+(n) < \epsilon \cdot \tau(n)\}\) is in fact \(\asymp \epsilon^{1 - o(1)}\), where the \(o(1)\) in the exponent tends to \(0\) as \(\epsilon \to 0\). Equivalently, \(\log(\text{upper density}) / \log \epsilon \to 1\) as \(\epsilon \to 0^+\).
theorem erdos_448.variants.erdos_tenenbaum :
Tendsto
(fun ε : ℝ =>
Real.log ({n : ℕ | (tauPlus n : ℝ) < ε * (n.divisors.card : ℝ)}.upperDensity) / Real.log ε)
(𝓝[>] (0 : ℝ)) (𝓝 (1 : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/448.lean, line 97.
Erdos448.erdos_448.variants.hall_tenenbaum_upper_bound
Solved: stated here without proof.
A more precise result of Hall and Tenenbaum [HaTe88, §4.6]: the upper density of \(\{n : \tau^+(n) < \epsilon \cdot \tau(n)\}\) is \(\ll \epsilon \cdot \log(2/\epsilon)\) as \(\epsilon \to 0^+\).
theorem erdos_448.variants.hall_tenenbaum_upper_bound :
(fun ε : ℝ => ({n : ℕ | (tauPlus n : ℝ) < ε * (n.divisors.card : ℝ)}).upperDensity)
=O[𝓝[>] (0 : ℝ)] (fun ε : ℝ => ε * Real.log (2 / ε))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/448.lean, line 109.
Erdos448.erdos_448.variants.hall_tenenbaum_distribution
Solved: stated here without proof.
Hall and Tenenbaum [HaTe88] further prove that \(\tau^+(n)/\tau(n)\) has a distribution function: there is a distribution function
F(non-decreasing, with \(F(-\infty) = 0\) and \(F(+\infty) = 1\)) such that, for every continuity point \(z\) ofF, the set \(\{n : \tau^+(n)/\tau(n) \le z\}\) has densityF z. Tenenbaum [Te13] proved thatFis continuous at \(z = 1\) and asked to determine its discontinuity points, if any.
theorem erdos_448.variants.hall_tenenbaum_distribution :
∃ F : ℝ → ℝ, Monotone F ∧ Tendsto F atBot (𝓝 0) ∧ Tendsto F atTop (𝓝 1) ∧
∀ z : ℝ, ContinuousAt F z →
{n : ℕ | (tauPlus n : ℝ) / (n.divisors.card : ℝ) ≤ z}.HasDensity (F z)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/448.lean, line 121.
Erdos448.erdos_448.variants.ford
Solved: stated here without proof.
Erdős and Graham asked whether there is a good inequality for \(\sum_{n \le x} \tau^+(n)\). This was answered by Ford [Fo08], who proved
\[ \sum_{n \le x} \tau^+(n) \asymp x \cdot \frac{(\log x)^{1 - \alpha}}{(\log\log x)^{3/2}}, \]where \(\alpha = 1 - \frac{1 + \log\log 2}{\log 2} = 0.08607\ldots\).
theorem erdos_448.variants.ford :
(fun x : ℕ => ∑ n ∈ Finset.Icc 1 x, (tauPlus n : ℝ))
=Θ[atTop]
(fun x : ℕ =>
let α : ℝ := 1 - (1 + Real.log (Real.log 2)) / Real.log 2
(x : ℝ) * Real.log (x : ℝ) ^ (1 - α)
/ Real.log (Real.log (x : ℝ)) ^ ((3 : ℝ) / 2))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/448.lean, line 133.
Sources
TheoremErdős Problem 450#
Reference: erdosproblems.com/450
Quoted from FormalConjectures/ErdosProblems/450.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/450.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos450.erdos_450
Open: stated without proof.
How large must \(y=y(\epsilon,n)\) be such that the number of integers in \((x,x+y)\) with a divisor in \((n,2n)\) is at most \(\epsilon y\)?
The bound is required for every \(x\) and every window length at least \(y\), and \(y(\epsilon,n)\) is the least such threshold (or \(\infty\) if there is none). A linear scale \(y \le C(\epsilon) n\) is known to suffice for fixed \(\epsilon\) and all large \(n\) (see
erdos_450.linear_scale_suffices).
theorem erdos_450 (ε : ℝ) (hε : 0 < ε) (n : ℕ) : windowThreshold ε n = erdos_450.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/450.lean, line 64.
Erdos450.erdos_450.linear_scale_suffices
Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-450/Research/TuranAnswer.lean.
A translate-uniform linear scale suffices: there is a sufficient window length
YwithY ε n ≤ C(ε) · n. This is an upper bound on the optimal scale, not the exact threshold asked for inerdos_450.
theorem erdos_450.linear_scale_suffices :
∃ Y : ℝ → ℕ → ℕ,
(∀ ε : ℝ, 0 < ε → ∃ C : ℝ, ∀ n : ℕ, (Y ε n : ℝ) ≤ C * n) ∧ IsSufficientScale Y
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/450.lean, line 74.
Sources
TheoremErdős Problem 452#
Reference: erdosproblems.com/452
Quoted from FormalConjectures/ErdosProblems/452.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/452.
The file states 1 research or textbook statement: 1 open.
Erdos452.erdos_452
Open: stated without proof.
Determine the largest length of an interval in \([x,2x]\) on which \(\omega(n) > \log\log n\) everywhere.
theorem erdos_452 : largeOmegaIntervalLength = erdos_452.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/452.lean, line 47.
Sources
TheoremErdős Problem 453#
References: - erdosproblems.com/453 - [Er70b] Erdős, P., Some applications of graph theory to number theory. Proc. Second Chapel Hill Conf. on Combinatorial Mathematics and its Applications (Univ. North Carolina, Chapel Hill, N.C., 1970) (1970), 136-145. - [Er74b] Erdős, P., Remarks on some problems in number theory. Math. Balkanica (1974), 197-202. - [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [Po79] Pomerance, Carl, The prime number graph. Math. Comp. (1979), 399-408.
Quoted from FormalConjectures/ErdosProblems/453.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/453.
The file states 1 research or textbook statement: 1 solved.
Erdos453.erdos_453
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos453.lean.
Is it true that, for all sufficiently large \(n\), there exists some \(i\lt n\) such that
\[ p_n^2 < p_{n+i}p_{n-i}, \]where \(p_k\) is the \(k\)th prime?
Pomerance proved that the answer is no.
theorem erdos_453 : ¬ EventuallyHasPrimeWitness
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/453.lean, line 61.
Sources
TheoremErdős Problem 454#
References: - erdosproblems.com/454 - [Po79] Pomerance, Carl, The prime number graph. Math. Comp. (1979), 399-408.
Quoted from FormalConjectures/ErdosProblems/454.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/454.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos454.erdos_454
Open: stated without proof.
Is it true that
limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop = ⊤?
theorem erdos_454 : limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop = ⊤
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/454.lean, line 40.
Erdos454.erdos_454.variants.two_le_limsup
Solved: stated here without proof.
limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop ≥ 2, and this is proved in [Po79].
theorem erdos_454.variants.two_le_limsup : 2 ≤ limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/454.lean, line 45.
Sources
TheoremErdős Problem 455#
References: - erdosproblems.com/455 - [Ri76] Richter, Bernd, Über die Monotonie von Differenzenfolgen. Acta Arith. (1976), 225-227.
Quoted from FormalConjectures/ErdosProblems/455.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/455.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos455.erdos_455
Open: stated without proof.
Let
q : ℕ → ℕbe a strictly increasing sequence of primes such thatq (n + 2) - q (n + 1) ≥ q (n + 1) - q n. Mustlim q n / (n ^ 2) = ∞?
theorem erdos_455: ∀ q : ℕ → ℕ, StrictMono q →
(∀ n, (q n).Prime ∧ q (n + 2) - q (n + 1) ≥ q (n + 1) - q n) →
Tendsto (fun n : ℕ => (q n : ℝ) / n ^ 2) atTop atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/455.lean, line 36.
Erdos455.erdos_455.variants.liminf
Solved: stated here without proof.
Let
q : ℕ → ℕbe a strictly increasing sequence of primes such thatq (n + 2) - q (n + 1) ≥ q (n + 1) - q n. Thenliminf q n / (n ^ 2) > 0.352, and this is proved in [Ri76].
theorem erdos_455.variants.liminf : ∀ q : ℕ → ℕ, StrictMono q →
(∀ n, (q n).Prime ∧ q (n + 2) - q (n + 1) ≥ q (n + 1) - q n) →
liminf (fun n : ℕ => (q n : ℝ≥0∞) / n ^ 2) atTop > 0.352
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/455.lean, line 45.
Sources
TheoremErdős Problem 456#
References: - erdosproblems.com/456 - [Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73--82.
Quoted from FormalConjectures/ErdosProblems/456.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/456.
The file states 7 research or textbook statements: 3 open, 3 solved and 1 textbook result.
Erdos456.erdos_456.parts.i
Open: stated without proof.
Is it true that \(m_n\lt p_n\) for almost all \(n\)?
theorem erdos_456.parts.i :
Tendsto (fun N ↦ (count (fun n ↦ m n < p n) N : ℝ) / (N : ℝ)) atTop (𝓝 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/456.lean, line 52.
Erdos456.erdos_456.parts.ii
Open: stated without proof.
Does \(p_n/m_n \to \infty\) for almost all \(n\)?
theorem erdos_456.parts.ii :
∃ A : Set ℕ, Tendsto (fun N ↦ (count (· ∈ A) N : ℝ) / (N : ℝ)) atTop (𝓝 1) ∧
Tendsto (fun n ↦ (p n : ℝ) / (m n : ℝ)) (atTop ⊓ 𝓟 A) atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/456.lean, line 61.
Erdos456.erdos_456.parts.iii
Open: stated without proof.
Are there infinitely many primes \(p\) such that \(p-1\) is the only \(n\) for which \(m_n=p\)?
theorem erdos_456.parts.iii :
{ q | q.Prime ∧ ∀ n, m n = q ↔ n = q - 1 }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/456.lean, line 70.
Erdos456.erdos_456.variants.linniks_theorem
Solved: stated here without proof.
Linnik's theorem implies that \(p_n\leq n^{O(1)}\).
theorem erdos_456.variants.linniks_theorem :
∃ L : ℝ, (fun n ↦ (p n : ℝ)) =O[atTop] (fun n ↦ (n : ℝ) ^ L)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/456.lean, line 78.
Erdos456.erdos_456.variants.mn_leq_pn
Textbook result, proved here.
It is trivial that \(m_n \leq p_n\) always.
theorem erdos_456.variants.mn_leq_pn (n : ℕ) :
m n ≤ p n
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/456.lean, line 86.
Erdos456.erdos_456.variants.infinitely_many_n
Proved here.
Erdős [Er79e] writes it is 'easy to show' that for infinitely many \(n\) we have \(m_n < p_n\).
theorem erdos_456.variants.infinitely_many_n :
{ n | m n < p n }.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/456.lean, line 114.
Erdos456.erdos_456.variants.m_div_n
Solved: stated here without proof.
Erdős [Er79e] writes it is 'easy to show' that \(m_n/n \to \infty\) for almost all \(n\).
theorem erdos_456.variants.m_div_n :
∃ A : Set ℕ, Tendsto (fun N ↦ (count (· ∈ A) N : ℝ) / N) atTop (𝓝 1) ∧
Tendsto (fun n ↦ (m n : ℝ) / (n : ℝ)) (atTop ⊓ 𝓟 A) atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/456.lean, line 161.
Sources
TheoremErdős Problem 457#
Reference: erdosproblems.com/457
Quoted from FormalConjectures/ErdosProblems/457.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/457.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos457.erdos_457
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem457.lean.
Is there some \(\epsilon > 0\) such that there are infinitely many \(n\) where all primes \(p \le (2 + \epsilon) \log n\) divide
\[ \prod_{1 \le i \le \log n} (n + i)? \]This was formalized in Lean by Baretto and van Doorn using Aristotle.
theorem erdos_457 : ∃ ε > (0 : ℝ),
{ (n : ℕ) | ∀ (p : ℕ), p ≤ (2 + ε) * Real.log n → p.Prime →
p ∣ ∏ i ∈ Finset.Icc 1 ⌊Real.log n⌋₊, (n + i) }.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/457.lean, line 41.
Erdos457.erdos_457.variants.qnk
Proved here.
More generally, let \(q(n, k)\) denote the least prime which does not divide \(\prod_{1 \le i \le k}(n + i)\). This problem asks whether \(q(n, \log n) \ge (2 + \epsilon) \log n\) infinitely often.
This follows from
erdos_457: if every prime \(p \le (2 + \epsilon) \log n\) divides \(\prod_{1 \le i \le \log n} (n + i)\), then \(q(n, \log n)\), the least prime not dividing this product, must exceed \((2 + \epsilon) \log n\).
theorem erdos_457.variants.qnk : ∃ ε > (0 : ℝ),
{ (n : ℕ) | (2 + ε) * Real.log n ≤ q n (Real.log n) }.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/457.lean, line 63.
Erdos457.erdos_457.variants.one_sub
Open: stated without proof.
Taking \(n\) to be the product of primes between \(\log n\) and \((2 + o(1)) \log n\) gives an example where
\[ q(n, \log n) \ge (2 + o(1)) \log n. \]Can one prove that \(q(n, \log n) < (1 - \epsilon) (\log n)^2\) for all large \(n\) and some \(\epsilon > 0\)?
theorem erdos_457.variants.one_sub : ∃ ε > (0 : ℝ),
∀ᶠ n in Filter.atTop, q n (Real.log n) < (1 - ε) * Real.log n ^ 2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/457.lean, line 84.
Sources
TheoremErdős Problem 458#
Reference: erdosproblems.com/458
Quoted from FormalConjectures/ErdosProblems/458.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/458.
The file states 1 research or textbook statement: 1 open.
Erdos458.erdos_458
Open: stated without proof.
Let \(\operatorname{lcm}(1, \dots, n)\) denote the least common multiple of \(\{1, \dots, n\}\). Let \(p_k\) be the \(k\)-th prime. Is it true that for all \(k \geq 1\), \(\operatorname{lcm}(1, \dots, p_{k+1}-1) < p_k \cdot \operatorname{lcm}(1, \dots, p_k)\)?
theorem erdos_458 :
∀ k : ℕ, lcm_upto ((k + 1).nth Prime - 1)
< k.nth Prime * lcm_upto (k.nth Prime)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/458.lean, line 41.
Sources
TheoremErdős Problem 459#
References: - erdosproblems.com/459 - [ErGr80] P. Erdős and R. L. Graham, Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique 28 (1980), p.91. - OEIS A289280
Quoted from FormalConjectures/ErdosProblems/459.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/459.
The file states 2 research or textbook statements: 2 solved.
Erdos459.erdos_459
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem459.lean.
Let \(f(u)\) be the largest \(v\) such that no \(m\in (u,v)\) is composed entirely of primes dividing \(uv\). Estimate \(f(u)\).
The estimate \(u + 2 \le f(u) \le u^2\) holds for every \(u \ge 2\). The upper bound is attained when \(u\) is prime, and the lower bound when \(u = 2^k - 2\) with \(k \ge 2\); Cambie further showed that \(f(n) = (1 + o(1))n\) for almost all \(n\).
theorem erdos_459 {u : ℕ} (hu : 2 ≤ u) : u + 2 ≤ f u ∧ f u ≤ u ^ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/459.lean, line 51.
Erdos459.erdos_459.variants.upper_tight
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem459.lean.
The upper bound \(f u ≤ u ^ 2\) is attained exactly when
uis prime: \(f p = p ^ 2\).
theorem erdos_459.variants.upper_tight {p : ℕ} (hp : p.Prime) : f p = p ^ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/459.lean, line 59.
Sources
TheoremErdős Problem 461#
References: - erdosproblems.com/461 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
Quoted from FormalConjectures/ErdosProblems/461.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/461.
The file states 1 research or textbook statement: 1 open. It also has 3 test statements and 1 API statement, counted here but not shown.
Erdos461.erdos_461
Open: stated without proof.
Let \(s_t(n)\) be the \(t\)-smooth component of \(n\) - that is, the product of all primes \(p\) (with multiplicity) dividing \(n\) such that \(p\lt t\). Let \(f(n,t)\) count the number of distinct possible values for \(s_t(m)\) for \(m\in [n+1,n+t]\). Is it true that
\[f(n,t)\gg t\](uniformly, for all \(t\) and \(n\))?
Erdős and Graham report they can show
\[f(n,t) \gg \frac{t}{\log t}.\]
theorem erdos_461 :
∃ c : ℝ, 0 < c ∧ ∀ n t : ℕ, c * (t : ℝ) ≤ (f n t : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/461.lean, line 53.
Sources
TheoremErdős Problem 462#
Reference: erdosproblems.com/462
Quoted from FormalConjectures/ErdosProblems/462.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/462.
The file states 1 research or textbook statement: 1 open.
Erdos462.erdos_462
Open: stated without proof.
Let \(p(n)\) denote the least prime factor of \(n\). Is there a constant \(C>0\) such that
\[\sum_{x\leq n\leq x+C\sqrt{x}(\log x)^2}\frac{p(n)}{n}\gg 1\]for all sufficiently large \(x\)?
theorem erdos_462 :
∃ C c : ℝ, 0 < C ∧ 0 < c ∧ ∀ᶠ x : ℕ in atTop,
c ≤ ∑ n ∈ Finset.Icc x
⌊(x : ℝ) + C * Real.sqrt x * (Real.log x) ^ 2⌋₊, (n.minFac : ℝ) / n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/462.lean, line 39.
Sources
TheoremErdős Problem 463#
Reference: erdosproblems.com/463
Quoted from FormalConjectures/ErdosProblems/463.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/463.
The file states 1 research or textbook statement: 1 open.
Erdos463.erdos_463
Open: stated without proof.
Is there a function \(f\) with \(f(n)\to\infty\) as \(n\to\infty\) such that, for all large \(n\), there is a composite number \(m\) such that
\[ n + f(n) < m < n + p(m) \]Here \(p(m)\) is the least prime factor of \(m\).
theorem erdos_463 : ∃ (f : ℕ → ℕ) (_ : Tendsto f atTop atTop),
∀ᶠ n in atTop,
∃ m, m.Composite ∧
n + f n < m ∧ m < n + m.minFac
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/463.lean, line 41.
Sources
TheoremErdős Problem 464#
References: - erdosproblems.com/464 - [Er75i] Erdős, P., Répartition modulo \(1\). (1975), iv+258. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980). - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [AkMo04] Akhunzhanov, R. K. and Moshchevitin, N. G., On the chromatic number of a distance graph associated with a lacunary sequence. Dokl. Akad. Nauk (2004), 295-296. - [Du06] Dubickas, Artūras, On the fractional parts of lacunary sequences. Math. Scand. (2006), 136-146. - [Ka01] Katznelson, Y., Chromatic numbers of Cayley graphs on \(\mathbb{Z}\) and recurrence. Combinatorica (2001), 211-219. - [PeSc10] Peres, Yuval and Schlag, Wilhelm, Two Erdős problems on lacunary sequences: chromatic number and Diophantine approximation. Bull. Lond. Math. Soc. (2010), 295-300. - [Po79b] Pollington, A. D., On the density of sequence \(\{n_k\xi\}\). Illinois J. Math. (1979), 511-515. - [dM80] de Mathan, B., Numbers contravening a condition in density modulo \(1\). Acta Math. Acad. Sci. Hungar. (1980), 237-241 (1981).
Quoted from FormalConjectures/ErdosProblems/464.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/464.
The file states 1 research or textbook statement: 1 solved.
Erdos464.erdos_464
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/110d489ed5c07e5b216453e092e9113127c98c9a/problems/464/Erdos464.lean.
Let \(A=\{n_1\lt n_2\lt \cdots\}\subset \mathbb{N}\) be a lacunary sequence (so there exists some \(\epsilon>0\) with \(n_{k+1}\geq (1+\epsilon)n_k\) for all \(k\)). Must there exist an irrational \(\theta\) such that
\[\{ \|\theta n_k\| : k\geq 1\}\]is not dense in \([0,1]\) (where \(\| x\|\) is the distance to the nearest integer)?
Solved independently by de Mathan [dM80] and Pollington [Po79b], who showed that, given any such \(A\), there exists such a \(\theta\), with
\[\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon^4}{\log(1/\epsilon)}.\]This bound was improved by Katznelson [Ka01], Akhunzhanov and Moshchevitin [AkMo04], and Dubickas [Du06], before Peres and Schlag [PeSc10] improved it to
\[\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon}{\log(1/\epsilon)},\]and note that the best bound possible here would be \(\gg \epsilon\).
This problem has consequences for 894.
The conclusion "\(\{\|\theta n_k\|\}\) is not dense in \([0,1]\)" is formalized as the sequence \((\theta n_k)\) not being dense modulo one; see the formalization notes above.
theorem erdos_464 :
∀ n : ℕ → ℕ, StrictMono n → (∀ k, 0 < n k) → IsLacunary n →
∃ θ : ℝ, Irrational θ ∧
¬ Dense (Set.range fun k => (↑(θ * n k) : AddCircle (1 : ℝ)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/464.lean, line 85.
Sources
TheoremErdős Problem 466#
References: - erdosproblems.com/466 - [Er72] Erdős, Paul, Extremal problems in number theory. Proceedings of the 1972 Number Theory Conference (Univ. Colorado, Boulder, Colo.) (1972), 80-86. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59-79. - [Sa76] Sárközy, A., On distances near integers. I, II. Studia Sci. Math. Hungar. (1976), 37-50, 105-111.
Quoted from FormalConjectures/ErdosProblems/466.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/466.
The file states 3 research or textbook statements: 3 solved.
Erdos466.erdos_466
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos466.lean#L292.
Let \(N(X,\delta)\) denote the maximum number of points \(P_1,\ldots,P_n\) which can be chosen in a circle of radius \(X\) such that
\[\| \lvert P_i-P_j\rvert \| \geq \delta\]for all \(1\leq i\lt j\leq n\). (Here \(\|x\|\) is the distance from \(x\) to the nearest integer.)
Is there some \(\delta>0\) such that
\[\lim_{X\to \infty}N(X,\delta)=\infty?\]Graham proved this is true, and in fact \(N(X,1/10)> \frac{\log X}{10}\). This was substantially improved by Sárközy [Sa76], who proved that for all sufficiently small \(\delta>0\), \(N(X,\delta)>X^{1/2-\delta^{1/7}}\).
theorem erdos_466 : ∃ δ : ℝ, 0 < δ ∧ Tendsto (fun X ↦ N X δ) atTop atTop
Category research solved; AMS 11 Number theory, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/466.lean, line 66.
Erdos466.erdos_466.variants.graham
Solved: stated here without proof.
Graham proved that \(N(X,1/10)> \frac{\log X}{10}\).
theorem erdos_466.variants.graham : ∀ X : ℝ, 1 ≤ X → Real.log X / 10 < N X (1 / 10)
Category research solved; AMS 11 Number theory, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/466.lean, line 71.
Erdos466.erdos_466.variants.sarkozy
Solved: stated here without proof.
Sárközy [Sa76] proved that for all sufficiently small \(\delta>0\), \(N(X,\delta)>X^{1/2-\delta^{1/7}}\) for all sufficiently large \(X\).
theorem erdos_466.variants.sarkozy : ∃ δ₀ : ℝ, 0 < δ₀ ∧ ∀ δ : ℝ, 0 < δ → δ < δ₀ →
∀ᶠ X : ℝ in atTop, X ^ (1 / 2 - δ ^ (1 / 7 : ℝ)) < N X δ
Category research solved; AMS 11 Number theory, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/466.lean, line 79.
Sources
TheoremErdős Problem 467#
Reference: erdosproblems.com/467
Quoted from FormalConjectures/ErdosProblems/467.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/467.
The file states 1 research or textbook statement: 1 open.
Erdos467.erdos_467
Open: stated without proof.
For every sufficiently large \(x\), choose a congruence class \(a_p\pmod p\) for each prime \(p\leq x\). Can the primes be decomposed into two nonempty sets \(A\) and \(B\) such that every \(n\lt x\) lies in a chosen class from \(A\) and in a chosen class from \(B\)?
This follows the interpretation on the Erdős Problems website, which notes that the original source omits some crucial quantifiers.
theorem erdos_467 :
∀ᶠ x in atTop, ∃ residue : ℕ → ℕ, ∃ A B : Finset ℕ,
PrimePartitionUpTo x A B ∧ CongruenceCover x residue A B
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/467.lean, line 62.
Sources
TheoremErdős Problem 469#
References: - erdosproblems.com/469 - [Le25] Lewis, Z. J., On the convergence of the reciprocal sum of primitive pseudoperfect numbers. Preprint (2025).
Quoted from FormalConjectures/ErdosProblems/469.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/469.
The file states 1 research or textbook statement: 1 solved.
Erdos469.erdos_469
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos469.lean.
Let \(A\) be the set of all \(n\) such that \(n = d_1 + ⋯ + d_k\) with \(d_i\) distinct proper divisors of \(n\), but this is not true for any \(m ∣ n\) with \(m < n\). Does:
\[ \sum_{n ∈ A} \frac 1 n \]converge?
Yes: the sum converges. This was proved by Lewis [Le25], whose proof has been formalized in Lean.
theorem erdos_469 :
letI A := {n : ℕ | 0 < n ∧ n.IsSumDivisors ∧ ∀ m < n, m ∣ n → ¬ m.IsSumDivisors}
Summable fun n : A ↦ 1 / (n : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/469.lean, line 52.
Sources
TheoremErdős Problem 470#
Reference: erdosproblems.com/470
Quoted from FormalConjectures/ErdosProblems/470.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/470.
The file states 8 research or textbook statements: 2 open, 5 solved and 1 textbook result.
Erdos470.erdos_470.parts.i
Open: stated without proof.
Are there any odd weird numbers?
theorem erdos_470.parts.i : ∃ n : ℕ, n.Weird ∧ Odd n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/470.lean, line 44.
Erdos470.erdos_470.parts.ii
Open: stated without proof.
Are there infinitely many primitive weird numbers?
theorem erdos_470.parts.ii : Set.Infinite PrimitiveWeird
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/470.lean, line 51.
Erdos470.erdos_470.variants.weird_pos_density
Solved: stated here without proof.
Benkoski and Erdős BeEr74 proved that the set of weird numbers has positive density.
HasPosDensityis the right reading here, rather than the positive lower density that Erdős' "positive density" usually abbreviates. Their Theorem 5 is stated as "the density of weird numbers is positive", and they first establish that the density exists at all: "It is clear that the weird numbers have a density since both the abundant numbers and the pseudoperfect numbers have a density. (A weird number is abundant and not pseudoperfect.)" The work in the paper goes into showing that density is not0.
theorem erdos_470.variants.weird_pos_density : {n : ℕ | n.Weird}.HasPosDensity
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/470.lean, line 66.
Erdos470.erdos_470.variants.smallest_weird_eq_70
Textbook result, proved here.
The smallest weird number is 70.
theorem erdos_470.variants.smallest_weird_eq_70 : (∀ n < 70, ¬n.Weird) ∧ (70).Weird
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/470.lean, line 73.
Erdos470.erdos_470.variants.prime_gap_imp_inf_prim_weird
Solved: stated here without proof.
Melfi Me15 has proved that there are infinitely many primitive weird numbers, conditional on the fact that \(p_{n+1} - p_n < \frac{1}{10} \sqrt{p_n}\) for all large \(n\), which in turn would follow from well-known conjectures concerning prime gaps.
theorem erdos_470.variants.prime_gap_imp_inf_prim_weird :
(∀ᶠ n in Filter.atTop, primeGap n < √ (n.nth Nat.Prime) / 10) →
Set.Infinite PrimitiveWeird
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/470.lean, line 104.
Erdos470.erdos_470.variants.odd_weird_10_pow_21
Solved: stated here without proof.
Fang Fa22 has shown there are no odd weird numbers below \(10^{21}\).
theorem erdos_470.variants.odd_weird_10_pow_21 : ∀ n < 10 ^ 21, Odd n → ¬n.Weird
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/470.lean, line 113.
Erdos470.erdos_470.variants.odd_weird_prime_div
Solved: stated here without proof.
Liddy and Riedl LiRi18 have shown that an odd weird number must have at least 6 prime divisors.
theorem erdos_470.variants.odd_weird_prime_div :
∀ n : ℕ, Odd n → n.Weird → 6 ≤ {m | m ∈ n.divisors ∧ m.Prime}.ncard
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/470.lean, line 121.
Erdos470.erdos_470.variants.abundancy_index
Solved: stated here; a Lean proof is at https://github.com/HowieHwong/lean-erdos-proofs/blob/40216cfee225ec5c9f122a48703e671a9f47db90/Erdos/P470.lean#L88.
If there are no odd weird numbers then every weird number has abundancy index < 4.
theorem erdos_470.variants.abundancy_index :
(∀ n : ℕ, n.Weird → ¬Odd n) → ∀ n, n.Weird → AbundancyIndex n < 4
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/470.lean, line 131.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.