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
The set of where is prime is an example of a good set. Formal proof provided by AlphaProof
Erdos12.IsGood {x | ∃ p, ∃ (_ : p ≡ 3 [MOD 4]) (_ : Nat.Prime p), p ^ 2 = x}