Erdős Problem 125

Reference: erdosproblems.com/125

theorem Erdos125.erdos_125 : sorry ↔ ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).HasPosDensity