module
public import Mathlib.Algebra.Group.Nat.Even
public import Mathlib.Algebra.Order.GroupWithZero.Basic
public import Mathlib.Algebra.Ring.Parity
public import Mathlib.Data.Nat.Choose.Basic
public import Mathlib.Data.Nat.Digits.Defs
public import Mathlib.Order.Interval.Finset.Nat
public import Mathlib.Order.Monotone.Basic
public import Mathlib.Tactic
public section
/-!
# International Mathematical Olympiad 1994, Problem 3
For any positive integer k, let f(k) be the number of elements in the set
{k+1, k+2, ... , 2k} which have exactly three 1s when written in base 2.
Prove that for each positive integer m, there is at least one k with f(k) = m,
and determine all m for which there is exactly one k.
-/
namespace Imo1994P3
/-- The number of `1`s in the binary representation of `n`. -/
def ones (n : ℕ) : ℕ := (Nat.digits 2 n).sum
/-- The function `f` of the problem: the number of elements of `{k+1, ..., 2k}`
whose binary representation has exactly three `1`s. -/
def f (k : ℕ) : ℕ := ((Finset.Icc (k + 1) (2 * k)).filter fun n => ones n = 3).card
/- determine -/ abbrev answer : Set ℕ := sorry
theorem imo1994_p3a : ∀ m : ℕ, 0 < m → ∃ k : ℕ, 0 < k ∧ f k = m := sorry
theorem imo1994_p3b : {m : ℕ | 0 < m ∧ ∃! k : ℕ, 0 < k ∧ f k = m} = answer := sorry
end Imo1994P3
This problem has a complete formalized solution.