Erdős Problem 602

Exercise 602 · Erdős

The formal statement below is all there is.

Formal statement · Lean 4.lean

private lemma evens_infinite : Set.Infinite {n : ℕ | Even n} := by
  sorry

Proof. sorry

Nobody has tried yet.