Erdős problem 318
There exists a set A with positive density that does not have property P₁. #TODO: prove this lemma by assuming erdos_318.contain_single_even.
Sources
FormalConjectures/ErdosProblems/
318.lean
Retained formal statement
The set of squares does not have property P₁.
¬Erdos318.P₁ {n | IsSquare n}TestStatement only, no proof