## Compfiles: Catalog Of Math Problems Formalized In Lean

## Usa2002P1

```
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finite.Basic
import Mathlib.Tactic
/-!
# USA Mathematical Olympiad 2002, Problem 1
Let S be a set with 2002 elements, and let N be an integer with
0 ≤ N ≤ 2^2002.
Prove that it is possible to color every subset of S either blue or
red so that the following conditions hold:
a) the union of any two red subsets is red;
b) the union of any two blue subsets is blue;
c) there are exactly N red subsets.
-/
namespace Usa2002P1
inductive Color : Type where
| red : Color
| blue : Color
deriving DecidableEq, Fintype
theorem usa2002_p1
{α : Type} [DecidableEq α] [Fintype α] (hs : Fintype.card α = 2002)
(N : ℕ) (hN : N ≤ 2 ^ 2002) :
∃ f : Finset α → Color,
((∀ s1 s2 : Finset α, f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧
(Fintype.card
{ a : Finset α // f a = Color.red } = N)) := sorry
end Usa2002P1
```

File author(s): David Renshaw

This problem has a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org: