Erdős Problem 369 to Erdős Problem 392
TheoremErdős Problem 369#
References: - erdosproblems.com/369 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [EgSe76] Eggleton, R. B. and Selfridge, J. L., Consecutive integers with no large prime factors. J. Austral. Math. Soc. Ser. A (1976), 1--11. - [BFMW20] Bober, J. W. and Fretwell, D. and Martin, G. and Wooley, T. D., Smooth values of polynomials. J. Aust. Math. Soc. (2020), 245--261. - [BaWo98] Balog, Antal and Wooley, Trevor D., On strings of consecutive integers with no large prime factors. J. Austral. Math. Soc. Ser. A (1998), 266-276.
Quoted from FormalConjectures/ErdosProblems/369.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/369.
The file states 1 research or textbook statement: 1 solved.
Erdos369.erdos_369
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos369.lean.
Let \(\epsilon>0\) and \(k\geq 2\). Is it true that, for all sufficiently large \(n\), there is a sequence of \(k\) consecutive integers in \(\{1,\ldots,n\}\) all of which are \(n^\epsilon\)-smooth?
The problem is trivially true as written (simply taking \(\{1,\ldots,k\}\) and \(n>k^{1/\epsilon}\)). There are (at least) two possible variants which are non-trivial, and it is not clear which Erdős and Graham meant. We formalize the second: each \(m\in P\) (where \(P\) is the sequence of \(k\) consecutive integers sought for) must be in \([n/2,n]\). In this case a positive answer also follows directly from the result of Balog and Wooley [BaWo98] for infinitely many \(n\). Proving this is true for all large \(n\) does not follow immediately from [BaWo98], but can be deduced using a similar construction, as shown by SkyYang.
theorem erdos_369 :
∀ (ε : ℝ) (hε : 0 < ε) (k : ℕ) (hk : 2 ≤ k),
∀ᶠ (n : ℕ) in atTop, ∃ a : ℕ, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧
∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, (p : ℝ) ≤ (n : ℝ) ^ ε
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/369.lean, line 55.
Sources
TheoremErdős Problem 370#
Reference: erdosproblems.com/370
Quoted from FormalConjectures/ErdosProblems/370.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/370.
The file states 1 research or textbook statement: 1 solved.
Erdos370.erdos_370
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos370.lean; a Lean proof is at https://github.com/XC0R/formal-conjectures/blob/f58dea7d2cc5c9da2e050ec80a73e838b54a6dd2/FormalConjectures/ErdosProblems/370.lean#L73.
Are there infinitely many \(n\) such that the largest prime factor of \(n\) is \(< n^{\frac{1}{2}}\) and the largest prime factor of \(n + 1\) is \(< (n + 1)^{\frac{1}{2}}\).
Steinerberger has pointed out this problem has a trivial solution.
This was formalized in Lean by Alexeev using Aristotle.
theorem erdos_370 :
{ n | Nat.maxPrimeFac n < √n ∧ Nat.maxPrimeFac (n + 1) < √(n + 1) }.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/370.lean, line 42.
Sources
TheoremErdős Problem 371#
References: - erdosproblems.com/371 - [OAI26a] OpenAI, The joint Dickman law for consecutive integers. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-joint-Dickman-law-for-consecutive-integers-September-24-2026/paper.pdf
Quoted from FormalConjectures/ErdosProblems/371.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/371.
The file states 1 research or textbook statement: 1 solved.
Erdos371.erdos_371
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/JointDickman/PaperMain.lean#L21.
Let \(P(n)\) denote the largest prime factor of \(n\). Show that the set of \(n\) with \(P(n+1) > P(n)\) has density \(\frac{1}{2}\).
This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
theorem erdos_371 :
{ n | Nat.maxPrimeFac (n + 1) > Nat.maxPrimeFac n }.HasDensity (1/2)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/371.lean, line 43.
Sources
TheoremErdős Problem 372#
Reference: erdosproblems.com/372
Conjectured by Erdős and Pomerance. Proved by Balog, who showed the stronger quantitative result that this holds for \(\gg \sqrt{x}\) many \(n\leq x\), for all large \(x\).
Quoted from FormalConjectures/ErdosProblems/372.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/372.
The file states 1 research or textbook statement: 1 solved.
Erdos372.erdos_372
Solved: stated here without proof.
Let \(P(n)\) denote the largest prime factor of \(n\). There are infinitely many \(n\) such that \(P(n)>P(n+1)>P(n+2)\).
theorem erdos_372 :
{n : ℕ | Nat.maxPrimeFac n > Nat.maxPrimeFac (n + 1) ∧
Nat.maxPrimeFac (n + 1) > Nat.maxPrimeFac (n + 2)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/372.lean, line 38.
Sources
TheoremErdős Problem 373#
Reference: erdosproblems.com/373
Quoted from FormalConjectures/ErdosProblems/373.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/373.
The file states 5 research or textbook statements: 3 open and 2 solved.
Erdos373.erdos_373
Open: stated without proof.
Show that the equation
n!=a_1!a_2!···a_k!, withn−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.
theorem erdos_373 : S.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/373.lean, line 45.
Erdos373.erdos_373.variants.of_limit
Solved: stated here without proof.
Show that if
P(n(n+1)) / log n → ∞whereP(m)denotes the largest prime factor ofm, then the equationn!=a_1!a_2!···a_k!, withn−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.
theorem erdos_373.variants.of_limit
(H : Filter.atTop.Tendsto (fun (n : ℕ) => (n*(n+1)).maxPrimeFac / (n : ℝ).log) Filter.atTop) :
S.Finite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/373.lean, line 54.
Erdos373.erdos_373.variants.of_lower_bound
Solved: stated here without proof.
Show that if
P(n(n−1)) > 4 log nfor large enoughn, whereP(m)denotes the largest prime factor ofm, then the equationn!=a_1!a_2!···a_k!, withn−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.
theorem erdos_373.variants.of_lower_bound
(H : ∀ᶠ (n : ℕ) in Filter.atTop, 4*(n : ℝ).log < (n*(n-1 : ℕ)).maxPrimeFac) :
S.Finite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/373.lean, line 71.
Erdos373.erdos_373.variants.maximal_solution
Open: stated without proof.
Hickerson conjectured the largest solution the equation
n!=a_1!a_2!···a_k!, withn−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, is16!=14!5!2!.
theorem erdos_373.variants.maximal_solution :
(16, [14, 5, 2]) ∈ S ∧ ∀ s ∈ S, s.fst ≤ 16
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/373.lean, line 81.
Erdos373.erdos_373.variants.suranyi
Open: stated without proof.
Surányi was the first to conjecture that the only non-trivial solution to
a!b!=n!is6!7!=10!.
theorem erdos_373.variants.suranyi :
{(n, a, b) : ℕ × ℕ × ℕ | n ! = a ! * b ! ∧ 1 < n ∧ 1 < a ∧ 1 < b ∧ b ≤ a ∧ a + 1 ≠ n}
= {(10, 7, 6)}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/373.lean, line 90.
Sources
TheoremErdős Problem 375#
References: - erdosproblems.com/375 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [RST75] Ramachandra, K. and Shorey, T. N. and Tijdeman, R., On Grimm's problem relating to factorisation of a block of consecutive integers. J. Reine Angew. Math. (1975), 109-124. -
Quoted from FormalConjectures/ErdosProblems/375.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/375.
The file states 5 research or textbook statements: 1 open and 4 solved.
Erdos375.erdos_375
Open: stated without proof.
Is
Erdos375Proptrue?
theorem erdos_375 : Erdos375Prop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/375.lean, line 47.
Erdos375.erdos_375.variants.bounded_gap
Solved: stated here without proof.
If
Erdos375Propis true, then(n + 1).nth Prime - n.nth Prime < (n.nth Prime) ^ (1 / 2 - c)for somec > 0.
theorem erdos_375.variants.bounded_gap : Erdos375Prop →
∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime
< (n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/375.lean, line 53.
Erdos375.erdos_375.variants.legendre
Proved here.
In particular, if
Erdos375Propis true, then Legendre's conjecture is asymptotically true.
theorem erdos_375.variants.legendre : Erdos375Prop →
(∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/375.lean, line 60.
Erdos375.erdos_375.variants.le_two
Proved here.
It is easy to see that for any
n ≥ 1andk ≤ 2, ifn + 1, ..., n + kare all composite, then there are distinct primesp₁, ... pₖsuch thatpᵢ ∣ n + ifor all1 ≤ i ≤ k.
theorem erdos_375.variants.le_two : ∀ n ≥ 1, ∀ k ≤ 2, (∀ i < k, ¬ (n + i + 1).Prime) →
∃ p : Fin k → ℕ, p.Injective ∧ ∀ i, (p i).Prime ∧ p i ∣ n + i + 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/375.lean, line 67.
Erdos375.erdos_375.variants.log
Solved: stated here without proof.
There exists a constant
c > 0such that for alln, ifk < c * (log n / (log (log n))) ^ 3 → (∀ i < k, ¬ (n + i + 1).Prime), then there are distinct primesp₁, ... pₖsuch thatpᵢ ∣ n + ifor all1 ≤ i ≤ k. This is proved in [RST75]. There is no need to only consider sufficiently largenbecause one can always takecsmall enough so thatk < c * (log n / (log (log n))) ^ 3implies thatk = 0untilnis large.
theorem erdos_375.variants.log : ∃ c > 0, ∀ n k : ℕ,
k < c * (Real.log n / (Real.log (Real.log n))) ^ 3 → (∀ i < k, ¬ (n + i + 1).Prime) →
∃ p : Fin k → ℕ, p.Injective ∧ ∀ i, (p i).Prime ∧ p i ∣ n + i + 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/375.lean, line 91.
Sources
TheoremErdős Problem 376#
Reference: erdosproblems.com/376
Quoted from FormalConjectures/ErdosProblems/376.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/376.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos376.erdos_376
Open: stated without proof.
Are there infinitely many \(n\) such that \({2n\choose n}\) is coprime to \(105\)?
theorem erdos_376 : { (n : ℕ) | n.centralBinom.Coprime 105 }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/376.lean, line 34.
Erdos376.erdos_376.variants.prime
Solved: stated here without proof.
Erdős, Graham, Ruzsa, and Straus [EGRS75] have shown that, for any two odd primes \(p\) and \(q\), there are infinite many \(n\) such that \({2n\choose n}\) is coprime to \(pq\).
theorem erdos_376.variants.prime {p q : ℕ} (h₁ : p.Prime)
(h₂ : Odd p) (h₃ : q.Prime) (h₄ : Odd q) :
{ (n : ℕ) | n.centralBinom.Coprime (p * q) }.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/376.lean, line 42.
Sources
TheoremErdős Problem 377#
Reference: erdosproblems.com/377
Quoted from FormalConjectures/ErdosProblems/377.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/377.
The file states 5 research or textbook statements: 1 open and 4 solved.
Erdos377.erdos_377
Open: stated without proof.
Is there some absolute constant \(C > 0\) such that
\[ \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} \leq C \]for all \(n\)?
theorem erdos_377 :
∃ C > (0 : ℝ), ∀ (n : ℕ), sumInvPrimesNotDvdCentralBinom n ≤ C
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/377.lean, line 49.
Erdos377.erdos_377.variants.limit.i
Solved: stated here without proof.
Erdos, Graham, Ruzsa, and Straus proved that if
\[ f(n) = \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} \]and
\[ \gamma_0 = \sum_{k = 2}^{\infty} \frac{\log k}{2^k} \]then
\[ \lim_{x\to\infty} \frac{1}{x}\sum_{n\leq x} f(n) = \gamma_0 \][EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of \(\binom{2n}{n}\). Math. Comp. (1975), 83-92.
theorem erdos_377.variants.limit.i (γ₀ : ℝ)
(hγ₀ : γ₀ = ∑' (k : ℕ), (k + 2 : ℝ).log / 2 ^ (k + 2)) :
Tendsto (fun (x : ℕ) => (1 : ℝ) / x * ∑ n ∈ Finset.Icc 1 x, sumInvPrimesNotDvdCentralBinom n)
atTop (𝓝 γ₀)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/377.lean, line 70.
Erdos377.erdos_377.variants.limit.ii
Solved: stated here without proof.
Erdos, Graham, Ruzsa, and Straus proved that if
\[ f(n) = \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} \]and
\[ \gamma_0 = \sum_{k = 2}^{\infty} \frac{\log k}{2^k} \]then
\[ \lim_{x\to\infty} \frac{1}{x}\sum_{n\leq x} f(n)^2 = \gamma_0^2 \][EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of \(\binom{2n}{n}\). Math. Comp. (1975), 83-92.
theorem erdos_377.variants.limit.ii (γ₀ : ℝ)
(hγ₀ : γ₀ = ∑' (k : ℕ), (k + 2 : ℝ).log / 2 ^ (k + 2)) :
Tendsto (fun (x : ℕ) =>
(1 : ℝ) / x * ∑ n ∈ Finset.Icc 1 x, sumInvPrimesNotDvdCentralBinom n ^ 2)
atTop (𝓝 (γ₀ ^ 2))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/377.lean, line 93.
Erdos377.erdos_377.variants.ae
Solved: stated here without proof.
Erdos, Graham, Ruzsa, and Straus proved that if
\[ f(n) = \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} \]and
\[ \gamma_0 = \sum_{k = 2}^{\infty} \frac{\log k}{2^k} \]then for almost all integers \(f(m) = \gamma_0 + o(1)\), i.e. for every \(\varepsilon > 0\) the set of \(n\) with \(|f(n) - \gamma_0| < \varepsilon\) has natural density one.
[EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of \(\binom{2n}{n}\). Math. Comp. (1975), 83-92.
theorem erdos_377.variants.ae (γ₀ : ℝ) (hγ₀ : γ₀ = ∑' (k : ℕ), (k + 2 : ℝ).log / 2 ^ (k + 2)) :
∀ ε > (0 : ℝ), {n : ℕ | |sumInvPrimesNotDvdCentralBinom n - γ₀| < ε}.HasDensity 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/377.lean, line 115.
Erdos377.erdos_377.variants.ub
Solved: stated here without proof.
Erdos, Graham, Ruzsa, and Straus proved that if
\[ f(n) = \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} \]then there is some constant \(c < 1\) such that for all large \(n\)
\[ f(n) \leq c \log\log n. \][EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of \(\binom{2n}{n}\). Math. Comp. (1975), 83-92.
theorem erdos_377.variants.ub : ∃ c < (1 : ℝ),
∀ᶠ n in atTop, sumInvPrimesNotDvdCentralBinom n ≤ c * (n : ℝ).log.log
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/377.lean, line 132.
Sources
TheoremErdős Problem 379#
Reference: erdosproblems.com/379
Quoted from FormalConjectures/ErdosProblems/379.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/379.
The file states 1 research or textbook statement: 1 solved.
Erdos379.erdos_379
Solved: stated here; a Lean proof is at https://github.com/teorth/analysis/blob/4f623b0f4cacdb967f1f8132db0becaee0f1fb3d/Analysis/Misc/erdos_379.lean#L90.
Let \(S(n)\) denote the largest integer such that, for all \(1 ≤ k < n\), the binomial coefficient \(\binom{n}{k}\) is divisible by \(p^S(n)\) for some prime \(p\) (depending on \(k\)).Then \(\limsup S(n) = \infty\).
This was formalized in Lean by Tao.
theorem erdos_379 : atTop.limsup (fun n => (S n : ℕ∞)) = ⊤
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/379.lean, line 45.
Sources
TheoremErdős Problem 382#
References: - erdosproblems.com/382 - [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/382.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/382.
The file states 4 research or textbook statements: 2 open, 1 solved and 1 textbook result. It also has 1 test statement, counted here but not shown.
Erdos382.lt_two_mul_of_largestPrimeRepeated
Textbook result, proved here.
If the condition holds, then \(v < 2u\).
Otherwise \(2u \leq v\), and by Bertrand's postulate there is a prime \(q\) with \(v/2 < q \leq v\), so \(u \leq q \leq v\). The largest prime \(p\) of the product satisfies \(p \geq q > v/2\). Hence \(p\) divides exactly one factor \(m \in [u, v]\), namely \(m = p\), and \(p\) appears with exponent \(1\).
theorem lt_two_mul_of_largestPrimeRepeated {u v : ℕ} (h : LargestPrimeRepeated u v) :
v < 2 * u
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/382.lean, line 59.
Erdos382.erdos_382.parts.i
Open: stated without proof.
Let \(u \leq v\) be such that the largest prime dividing \(\prod_{u \leq m \leq v} m\) appears with exponent at least \(2\). Is it true that \(v - u = v^{o(1)}\)?
We read this as: for every \(\epsilon > 0\), every such pair with \(v\) large enough satisfies \(v - u \leq v^{\epsilon}\). Cambie observed that this question reduces to old conjectures on gaps between primes; for example, it follows from Cramér's conjecture. See also Erdős Problems 380 and 383.
theorem erdos_382.parts.i :
∀ ε > (0 : ℝ), ∀ᶠ v : ℕ in atTop, ∀ u : ℕ, LargestPrimeRepeated u v →
((v - u : ℕ) : ℝ) ≤ (v : ℝ) ^ ε
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/382.lean, line 104.
Erdos382.erdos_382.parts.ii
Open: stated without proof.
Let \(u \leq v\) be such that the largest prime dividing \(\prod_{u \leq m \leq v} m\) appears with exponent at least \(2\). Can \(v - u\) be arbitrarily large?
That is, for every \(k\), is there such a pair with \(v - u \geq k\)? Cambie gives a heuristic that suggests the answer is yes.
theorem erdos_382.parts.ii :
∀ k : ℕ, ∃ u v : ℕ, LargestPrimeRepeated u v ∧ k ≤ v - u
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/382.lean, line 117.
Erdos382.erdos_382.variants.ramachandra
Solved: stated here without proof.
Erdős and Graham [ErGr80] report that it follows from results of Ramachandra that \(v - u \leq v^{1/2+o(1)}\) for every pair \(u \leq v\) as in
Erdos382.erdos_382.parts.i.That is, for every \(\epsilon > 0\), every such pair with \(v\) large enough satisfies \(v - u \leq v^{1/2+\epsilon}\).
theorem erdos_382.variants.ramachandra :
∀ ε > (0 : ℝ), ∀ᶠ v : ℕ in atTop, ∀ u : ℕ, LargestPrimeRepeated u v →
((v - u : ℕ) : ℝ) ≤ (v : ℝ) ^ ((1 : ℝ) / 2 + ε)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/382.lean, line 129.
Sources
TheoremErdős Problem 383#
Reference: erdosproblems.com/383
Quoted from FormalConjectures/ErdosProblems/383.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/383.
The file states 1 research or textbook statement: 1 open.
Erdos383.erdos_383
Open: stated without proof.
Is it true that for every \(k\) there are infinitely many primes \(p\) such that the largest prime divisor of
\[ \prod_{i = 0}^k (p ^ 2 + i) \]is \(p\)?
theorem erdos_383 :
∀ k, {p : ℕ | p.Prime ∧ Nat.maxPrimeFac (∏ i ∈ Finset.Icc 0 k, (p ^ 2 + i)) = p}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/383.lean, line 39.
Sources
TheoremErdős Problem 384#
References: - erdosproblems.com/384 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Ec69] Ecklund, Jr., E. F., On prime divisors of the binomial coefficient. Pacific J. Math. (1969), 267-270. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
Quoted from FormalConjectures/ErdosProblems/384.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/384.
The file states 2 research or textbook statements: 2 solved.
Erdos384.erdos_384
Solved: stated here without proof.
If \(1\lt k\lt n-1\) then \(\binom{n}{k}\) is divisible by a prime \(p\leq n/2\) (except \(\binom{7}{3}=\binom{7}{4}=5\cdot 7\)).
A conjecture of Erdős and Selfridge [ErGr80]. Proved by Ecklund [Ec69], who made the stronger conjecture that whenever \(n>k^2\) the binomial coefficient \(\binom{n}{k}\) is divisible by a prime \(p\lt n/k\). Discussed in problem B31 and B33 of Guy's collection [Gu04]. Stronger forms of this conjecture are 1094 and 1095.
Ecklund's theorem is stated for \(n \geq 2k\) with the single exception \(\binom{7}{3}\); by the symmetry \(\binom{n}{k} = \binom{n}{n-k}\) this is the form above, where \(\binom{7}{4}\) is the second exception. The prime bound is \(p \leq n/2\) (that is, \(2p \leq n\)); see
erdos_384.variants.strictfor the strict inequality.
theorem erdos_384 (n k : ℕ) (hk : 1 < k) (hkn : k < n - 1) (h₃ : (n, k) ≠ (7, 3))
(h₄ : (n, k) ≠ (7, 4)) :
∃ p : ℕ, p.Prime ∧ p ∣ n.choose k ∧ 2 * p ≤ n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/384.lean, line 52.
Erdos384.erdos_384.variants.strict
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos384.lean#L71.
With the strict inequality \(p < n/2\) the statement is false: \(\binom{4}{2} = 6\) has no prime divisor \(p < 2\).
theorem erdos_384.variants.strict :
¬ ∀ n k : ℕ, 1 < k → k < n - 1 → (n, k) ≠ (7, 3) → (n, k) ≠ (7, 4) →
∃ p : ℕ, p.Prime ∧ p ∣ n.choose k ∧ 2 * p < n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/384.lean, line 64.
Sources
TheoremErdős Problem 385#
Reference: erdosproblems.com/385
Quoted from FormalConjectures/ErdosProblems/385.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/385.
The file states 3 research or textbook statements: 3 open. It also has 1 test statement, counted here but not shown.
Erdos385.erdos_385.parts.i
Open: stated without proof.
Let \(F(n) := \max\{m + p(m) \mid \textrm{\)m < n$ composite}}}$ where \(p(m)\) is the least prime divisor of \(m\). Is it true that \(F(n)>n\) for all sufficiently large \(n\)?
theorem erdos_385.parts.i : ∀ᶠ n in atTop, n < F n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/385.lean, line 58.
Erdos385.erdos_385.parts.ii
Open: stated without proof.
Let \(F(n) := \max\{m + p(m) \mid \textrm{\)m < n$ composite}}}$ where \(p(m)\) is the least prime divisor of \(m\). Does \(F(n) - n \to \infty\) as \(n\to\infty\)?
theorem erdos_385.parts.ii : atTop.Tendsto (fun n ↦ F n - n) atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/385.lean, line 64.
Erdos385.erdos_385.variants.lb
Open: stated without proof.
A question of Erdős, Eggleton, and Selfridge, who write that in fact it is possible that this quantity is always at least \(n+(1-o(1))\sqrt{n}\)
theorem erdos_385.variants.lb : ∃ (e : ℕ → ℝ) (he : e =o[atTop] (1 : ℕ → ℝ)),
∀ n, n + (1 - e n) * √n ≤ F n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/385.lean, line 70.
Sources
TheoremErdős Problem 386#
Reference: erdosproblems.com/386
Quoted from FormalConjectures/ErdosProblems/386.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/386.
The file states 3 research or textbook statements: 3 open.
Erdos386.erdos_386
Open: stated without proof.
Let \(2 \le k \le n - 2\). Can \(\binom{n}{k}\) be the product of consecutive primes infinitely often? Here \(k\) may vary with \(n\): the question asks for infinitely many admissible binomial coefficients, not for a single \(k\) that works infinitely often.
theorem erdos_386 :
∃ᶠ n in .atTop, ∃ k ≥ 2,
k ≤ n - 2 ∧ ∃ p q : ℕ, n.choose k = ∏ i ∈ .Ico p q, nth Nat.Prime i
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/386.lean, line 38.
Erdos386.erdos_386.variants.forall
Open: stated without proof.
For all \(2 \le k \le n - 2\), can \(\binom{n}{k}\) be the product of consecutive primes infinitely often?
theorem erdos_386.variants.forall :
∀ k ≥ 2, ∃ᶠ n in .atTop,
k ≤ n - 2 ∧ ∃ p q : ℕ, n.choose k = ∏ i ∈ .Ico p q, nth Nat.Prime i
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/386.lean, line 48.
Erdos386.erdos_386.variants.two
Open: stated without proof.
Can \(\binom{n}{2}\) be the product of consecutive primes infinitely often?
theorem erdos_386.variants.two :
∃ᶠ n in .atTop,
2 ≤ n - 2 ∧ ∃ p q : ℕ, n.choose 2 = ∏ i ∈ .Ico p q, nth Nat.Prime i
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/386.lean, line 57.
Sources
TheoremErdős Problem 387#
References: - erdosproblems.com/387 - [ErGr76b] Erdős, P. and Graham, R. L., On the prime factors of \({n \choose k}\). Fibonacci Quart. (1976), 348-352. - [Er78g] Erdős, Pál, On prime factors of binomial coefficients. II. Mat. Lapok (1978/82), 307-316. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Sc58] Schinzel, A., Sur un problème de P. Erdős. Colloq. Math. (1958), 198-204. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [Fa66] Faulkner, M. "On a theorem of Sylvester and Schur." Journal of the London Mathematical Society 1.1 (1966): 107-110. - [BNPZ26] Bui, H., Naprienko, S., Pratt, K., and Zaharescu, A. Binomial coefficients with divisors avoiding an interval. arXiv:2605.21221 (2026).
Quoted from FormalConjectures/ErdosProblems/387.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/387.
The file states 4 research or textbook statements: 1 open and 3 solved.
Erdos387.erdos_387
Solved: stated here without proof.
Is there an absolute constant \(c > 0\) such that, for all \(1 \leq k < n\), the binomial coefficient \(\binom{n}{k}\) has a divisor in \((cn, n]\)?
Bui, Naprienko, Pratt, and Zaharescu [BNPZ26] answered this negatively.
theorem erdos_387 : ¬ ∃ c : ℝ, 0 < c ∧ ∀ n k : ℕ, 1 ≤ k → k < n →
∃ d : ℕ, (d : ℝ) ∈ Set.Ioc (c * n) n ∧ d ∣ n.choose k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/387.lean, line 52.
Erdos387.erdos_387.variants.schinzel
Open: stated without proof.
The following is Schinzel's conjecture, which appears in [Gu04].
theorem erdos_387.variants.schinzel :
∀ᶠ k in atTop, ¬ IsPrimePow k → ∃ n : ℕ, ∀ i < k, ¬ n - i ∣ n.choose k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/387.lean, line 62.
Erdos387.erdos_387.variants.easy
Proved here.
It is easy to see that
n.choose khas a divisor in[n / k, n].
theorem erdos_387.variants.easy {n : ℕ} {k : ℕ} (hn : 1 ≤ n) (hk : k ≤ n) : ∃ d : ℕ,
(d : ℝ) ∈ Set.Icc (n / k : ℝ) n ∧ d ∣ n.choose k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/387.lean, line 68.
Erdos387.erdos_387.variants.guy
Solved: stated here without proof.
Is it true for any \(c < 1\) and all \(n\) sufficiently large, for all \(1 \leq k < n\), \(\binom{n}{k}\) has a divisor in \((cn, n]\)?
This variant appears in [Gu04]. Bui, Naprienko, Pratt, and Zaharescu [BNPZ26] answered it negatively.
theorem erdos_387.variants.guy : ¬ ∀ c : ℝ, c < 1 → ∀ᶠ n : ℕ in atTop, ∀ k : ℕ, 1 ≤ k →
k < n → ∃ d : ℕ, (d : ℝ) ∈ Set.Ioc (c * n) n ∧ d ∣ n.choose k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/387.lean, line 88.
Sources
TheoremErdős Problem 388#
References: - erdosproblems.com/388 - [Er76d] Erdős, P., Problems and results on number theoretic properties of consecutive integers and related questions. Proceedings of the Fifth Manitoba Conference on Numerical Mathematics (Univ. Manitoba, Winnipeg, Man., 1975) (1976), 25-44. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48.
Quoted from FormalConjectures/ErdosProblems/388.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/388.
The file states 3 research or textbook statements: 3 open.
Erdos388.erdos_388
Open: stated without proof.
Are there only finitely many solutions of
\[\prod_{1\leq i\leq k_1}(m_1+i)=\prod_{1\leq j\leq k_2}(m_2+j)\]with \(k_1,k_2>3\) and \(m_1+k_1\leq m_2\)?
Here \(m_1, m_2 \geq 0\), so every factor is positive and the condition \(m_1 + k_1 \leq m_2\) makes the two blocks disjoint. Negative \(m_1\) would give trivial solutions such as \((-5)(-4)(-3)(-2) = 2 \cdot 3 \cdot 4 \cdot 5\). The source also asks to classify all solutions; see
Erdos388.erdos_388.variants.classification.
theorem erdos_388 :
{(m₁, k₁, m₂, k₂) : ℕ × ℕ × ℕ × ℕ | 3 < k₁ ∧ 3 < k₂ ∧ m₁ + k₁ ≤ m₂ ∧
∏ i ∈ Finset.Icc 1 k₁, (m₁ + i) = ∏ j ∈ Finset.Icc 1 k₂, (m₂ + j)}.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/388.lean, line 49.
Erdos388.erdos_388.variants.classification
Open: stated without proof.
Can one classify all solutions of
\[\prod_{1\leq i\leq k_1}(m_1+i)=\prod_{1\leq j\leq k_2}(m_2+j)\]with \(k_1,k_2>3\) and \(m_1+k_1\leq m_2\)?
A solution must supply the set of all solutions \((m_1, k_1, m_2, k_2)\). Whether a description of this set is a satisfactory classification is up to human judgement.
theorem erdos_388.variants.classification :
{(m₁, k₁, m₂, k₂) : ℕ × ℕ × ℕ × ℕ | 3 < k₁ ∧ 3 < k₂ ∧ m₁ + k₁ ≤ m₂ ∧
∏ i ∈ Finset.Icc 1 k₁, (m₁ + i) = ∏ j ∈ Finset.Icc 1 k₂,
(m₂ + j)} = erdos_388.variants.classification.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/388.lean, line 65.
Erdos388.erdos_388.variants.general
Open: stated without proof.
More generally, if \(k_1>2\) then for fixed \(a\) and \(b\) the equation
\[a\prod_{1\leq i\leq k_1}(m_1+i)=b\prod_{1\leq j\leq k_2}(m_2+j)\]should have only finitely many solutions.
The source states no condition on \(a\), \(b\), \(k_2\) or the position of the blocks, so this is our reading: \(a\) and \(b\) are positive integers, we keep the condition \(m_1+k_1\leq m_2\) of the main problem (the \(k_1\)-block lies below the \(k_2\)-block), and we assume \(k_2 > 2\) as well. Without these conditions there are infinite families of solutions: - for \(k_2 = 1\) and \(b = 1\), take \(m_2 + 1 = a\prod_{1\leq i\leq k_1}(m_1+i)\); - for \(k_2 = 2\), \(a = 1\) and \(b = 4\), the identity \((n+1)(n+2)(n+3)(n+4) = Y(Y+2)\) with \(Y = (n+1)(n+4)\) even gives a solution with \(m_2 + 1 = Y/2\) for every \(n \geq 2\); - overlapping blocks give \(2\prod_{1\leq i\leq k}(k-1+i)=\prod_{1\leq j\leq k}(k+j)\) for every \(k \geq 2\).
theorem erdos_388.variants.general (a b : ℕ) (ha : 0 < a) (hb : 0 < b) :
{(m₁, k₁, m₂, k₂) : ℕ × ℕ × ℕ × ℕ | 2 < k₁ ∧ 2 < k₂ ∧ m₁ + k₁ ≤ m₂ ∧
a * ∏ i ∈ Finset.Icc 1 k₁, (m₁ + i) = b * ∏ j ∈ Finset.Icc 1 k₂, (m₂ + j)}.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/388.lean, line 87.
Sources
TheoremErdős Problem 389#
Reference: erdosproblems.com/389
Quoted from FormalConjectures/ErdosProblems/389.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/389.
The file states 2 research or textbook statements: 1 open and 1 textbook result.
Erdos389.erdos_389
Open: stated without proof.
Is it true that for every \(n \geq 1\) there is a \(k\) such that
\[ n(n + 1) \cdots (n + k - 1) \mid (n + k) \cdots (n + 2k - 1)? \]
theorem erdos_389 :
∀ n ≥ 1, ∃ k ≥ 1, ∏ i ∈ Finset.range k, (n + i) ∣ ∏ i ∈ Finset.range k, (n + k + i)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/389.lean, line 37.
Erdos389.erdos_389.variants.mehta_four
Textbook result, proved here.
Bhavik Mehta has computed the minimal such \(k\) for \(1 \leq n \leq 18\). For example, the minimal \(k\) for \(n = 4\) is \(207\).
theorem erdos_389.variants.mehta_four :
IsLeast
{ k | 1 ≤ k ∧ ∏ i ∈ Finset.range k, (4 + i) ∣ ∏ i ∈ Finset.range k, (4 + k + i) }
207
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/389.lean, line 46.
Sources
TheoremErdős Problem 390#
References: - erdosproblems.com/390 - [EGS82] Erdős, P., R. K. Guy, and J. L. Selfridge. "Another Property of 239 and some related questions." Congr. Numer. 34 (1982): 243-257. -
Quoted from FormalConjectures/ErdosProblems/390.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/390.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos390.erdos_390.variants.theta
Solved: stated here without proof.
f n - 2 * n = θ (n / log n). This is proved in [EGS82].
theorem erdos_390.variants.theta :
(fun n => f n - 2 * n : ℕ → ℝ) =Θ[atTop] (fun n => n / log (n : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/390.lean, line 44.
Erdos390.erdos_390
Open: stated without proof.
Does there exists a constant
csuch thatf n - 2 * n ~ c * (n / log n)?
theorem erdos_390 :
∃ c,
(fun n => f n - 2 * n : ℕ → ℝ) ~[atTop] (fun n => c * n / log (n : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/390.lean, line 50.
Sources
TheoremErdős Problem 391#
References: - erdosproblems.com/391 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er96b] Erdős, Paul, Some problems I presented or planned to present in my short talk. Analytic number theory, Vol. 1 (Allerton Park, IL, 1995) (1996), 333-335. - [AlGr77] Alladi, Krishnaswami and Grinstead, Charles, On the decomposition of \(n!\) into prime powers. J. Number Theory (1977), 452-458. - [ACRSTUV25] B. Alexeev, E. Conway, M. Rosenfeld, A. Sutherland, T. Tao, M. Uhr, and K. Ventullo, Decomposing a factorial into large factors. arXiv:2503.20170 (2025).
Quoted from FormalConjectures/ErdosProblems/391.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/391.
The file states 2 research or textbook statements: 2 solved.
Erdos391.erdos_391
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos391.lean#L4924.
Let \(t(n)\) be maximal such that there is a representation
\[n!=a_1\cdots a_n\]with \(t(n)=a_1\leq \cdots \leq a_n\). Obtain good bounds for \(t(n)/n\). In particular, is it true that
\[\lim \frac{t(n)}{n}=\frac{1}{e}?\]It is easy to see that \(\lim \frac{t(n)}{n}\leq \frac{1}{e}\). Erdős [Er96b] wrote he, Selfridge, and Straus had proved a corresponding lower bound, so that \(\lim \frac{t(n)}{n}=\frac{1}{e}\), and 'believed that Straus had written up our proof. Unfortunately Straus suddenly died and no trace was ever found of his notes. Furthermore, we never could reconstruct our proof, so our assertion now can be called only a conjecture.'
Alladi and Grinstead [AlGr77] have obtained similar results when the \(a_i\) are restricted to prime powers.
Both questions were answered by Alexeev, Conway, Rosenfeld, Sutherland, Tao, Uhr, and Ventullo [ACRSTUV25], who proved that
\[\frac{t(n)}{n}= \frac{1}{e}-\frac{c_0}{\log n}+O\left(\frac{1}{(\log n)^{1+c}}\right),\]where \(c_0=0.3044\cdots\) is an explicit constant, for some \(c>0\).
theorem erdos_391 :
Tendsto (fun n : ℕ => (t n : ℝ) / n) atTop (𝓝 (1 / Real.exp 1))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/391.lean, line 70.
Erdos391.erdos_391.variants.deficit
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos391.lean#L4924.
Furthermore, does there exist some constant \(c>0\) such that
\[\frac{t(n)}{n} \leq \frac{1}{e}-\frac{c}{\log n}\]for infinitely many \(n\)?
This was answered in the affirmative by Alexeev, Conway, Rosenfeld, Sutherland, Tao, Uhr, and Ventullo [ACRSTUV25].
theorem erdos_391.variants.deficit : ∃ c : ℝ, 0 < c ∧
{n : ℕ | (t n : ℝ) / n ≤ 1 / Real.exp 1 - c / Real.log n}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/391.lean, line 85.
Sources
TheoremErdős Problem 392#
Reference: erdosproblems.com/392
Quoted from FormalConjectures/ErdosProblems/392.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/392.
The file states 3 research or textbook statements: 3 solved.
Erdos392.erdos_392
Solved: stated here; a Lean proof is at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/d82a35ecc798ada27f82a88b559f25b753f63a73/PrimeNumberTheoremAnd/IEANTN/Erdos392.lean.
Let \(A(n)\) denote the least value of \(t\) such that
\[ n! = a_1 \cdots a_t \]with \(a_1 \leq \cdots \leq a_t\leq n^2\). Then
\[ A(n) = \frac{n}{2} - \frac{n}{2\log n} + o\left(\frac{n}{\log n}\right). \]
theorem erdos_392 (A : ℕ → ℕ) (h : ∀ n > 0,
IsLeast { t + 1 | (t) (_ : ∃ a : Fin (t + 1) → ℕ, (n)! = ∏ i, a i ∧
Monotone a ∧ a (Fin.last t) ≤ n ^ 2) } (A n)) :
((fun (n : ℕ) => (A n - n / 2 + n / (2 * Real.log n) : ℝ)) =o[atTop] fun n => n / Real.log n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/392.lean, line 46.
Erdos392.erdos_392.variants.lower
Solved: stated here without proof.
If we change the condition to \(a_t \leq n\) it can be shown that
\[ A(n) = n - \frac{n}{\log n} + o\left(\frac{n}{\log n}\right) \]
theorem erdos_392.variants.lower (A : ℕ → ℕ)
(hA : ∀ n > 0, IsLeast
{ t + 1 | (t) (_ : ∃ a : Fin (t + 1) → ℕ, (n)! = ∏ i, a i ∧
Monotone a ∧ a (Fin.last t) ≤ n) } (A n)) :
(fun (n : ℕ) => (A n - n + n / Real.log n : ℝ)) =o[atTop] fun n => n / Real.log n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/392.lean, line 60.
Erdos392.erdos_392.variants.implication
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos392_erdos_392_variants_implication.lean#L177.
Cambie has observed that a positive answer follows from the result above with \(a_t \leq n\), simply by pairing variables together, e.g. taking \(a'_i = a_{2i-1}a_{2i}\) (and the lower bound follows from Stirling's approximation).
theorem erdos_392.variants.implication (h : type_of% erdos_392.variants.lower) :
type_of% erdos_392
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/392.lean, line 74.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.