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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/457.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:457
  • PLBY Lean proofsErdosProblems.Erdos457

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry