Erdős problem 12
Let be infinite with no distinct such that with . Can have positive lower limit? Must every such fall below infinitely often?
Sources
FormalConjectures/ErdosProblems/
12.lean
Retained formal statement
An example of an with the property that there are no distinct such that and and such that is given by the set of , where is prime.
∀ (A : Set ℕ), A = {x | ∃ p, ∃ (_ : Nat.Prime p) (_ : p ≡ 3 [MOD 4]), p ^ 2 = x} → Erdos12.IsGood A ∧ 0 < Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard * Real.log ↑N / √↑N) Filter.atTopSolvedStatement only, no proof