## Compfiles: Catalog Of Math Problems Formalized In Lean

## Usa2001P1

```
import Mathlib.Data.Finset.Card
import Mathlib.Order.Bounds.Basic
import Mathlib.Tactic
/-!
# USA Mathematical Olympiad 2001, Problem 1
Each of eight boxes contains six balls.
Each ball has been colored with one of n colors, such that no two balls
in the same box are the same color, and no two colors occur together in
more than one box. Determine, with justification, the smallest integer n
for which this is possible.
-/
namespace Usa2001P1
def possible_num_colors : Set ℕ :=
{ n : ℕ | ∃ f : Fin 8 → Finset (Fin n),
(∀ i, (f i).card = 6) ∧
(∀ x y : Fin n, ∀ i j : Fin 8,
i ≠ j → x ∈ f i → y ∈ f i →
(¬ (x ∈ f j ∧ y ∈ f j))) }
/- determine -/ abbrev min_colors : ℕ := sorry
theorem usa2001_p1 : IsLeast possible_num_colors min_colors := sorry
end Usa2001P1
```

File author(s): David Renshaw

This problem does not yet have a complete formalized solution.

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