AIME_2021_3.lean

import data.finset.basic


theorem AIME_2021_3 (S:finset ℕ)(h:∀(n:ℕ), n∈S ↔ (n≤ 1000 ∧ ∃ (a b :ℕ),n=2^a-2^b)): finset.card S=50 :=
begin
  sorry
end