Erdős problem 692
Let be the density of the set of integers with exactly one divisor in . Is unimodular for (i.e. increases until some then decreases thereafter)?
Sources
FormalConjectures/ErdosProblems/
692.lean
Retained formal statement
Let be the density of the set of integers with exactly one divisor in . For fixed , where does achieve its maximum?
∀ (n : ℕ) (δ : ℕ → ℕ → ℝ), (∀ (a b : ℕ), Erdos692.IsDelta₁ a b (δ a b)) → IsGreatest (δ n '' Set.Ioi (n + 1)) (δ n sorry)OpenStatement only, no proof