Skip to content

Erdős problem 457

Start work

Is there some ϵ>0\epsilon > 0 such that there are infinitely many nn where all primes p≤(2+ϵ)log⁡np \le (2 + \epsilon) \log n divide ∏1≤i≤log⁡n(n+i)? \prod_{1 \le i \le \log n} (n + i)?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

457.lean

Retained formal statement1 of 3

Is there some ϵ>0\epsilon > 0 such that there are infinitely many nn where all primes p≤(2+ϵ)log⁡np \le (2 + \epsilon) \log n divide ∏1≤i≤log⁡n(n+i)? \prod_{1 \le i \le \log n} (n + i)?

This was formalized in Lean by Baretto and van Doorn using Aristotle.

FormalConjectures/ErdosProblems/457.leanErdos457.erdos_4573 linesExact file
True ↔  ∃ ε > 0,    {n | ∀ (p : ℕ), ↑p ≤ (2 + ε) * Real.log ↑n → Nat.Prime p → p ∣ ∏ i ∈ Finset.Icc 1 ⌊Real.log ↑n⌋₊, (n + i)}.Infinite
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.