Erdős Problem 371

Conjecture 371 · Erdős

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}$ .

Formal statement · Lean 4.lean

theorem erdos_371 :
    { n | Nat.maxPrimeFac (n + 1) > Nat.maxPrimeFac n }.HasDensity (1/2) := by
  sorry

Proof. sorry

Nobody has tried yet.