Erdős problem 457 · problems.science

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)?$

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

457.lean

Retained formal statement1 of 3

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.

FormalConjectures/ErdosProblems/457.leanErdos457.erdos_4573 linesExact file

1True ↔2  ∃ ε > 0,3    {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.

Sources

Search problems.science