## Compfiles: Catalog Of Math Problems Formalized In Lean

## Bulgaria1998P1

```
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.IntervalCases
/-!
# Bulgarian Mathematical Olympiad 1998, Problem 1
We will be considering colorings in 2 colors of n (distinct) points
A₁, A₂, ..., Aₙ. Call such a coloring "good" if there exist three points
Aᵢ, Aⱼ, A₂ⱼ₋ᵢ, 1 ≤ i < 2j - i ≤ n, which are colored the same color.
Find the least natural number n (n ≥ 3) such that all colorings
of n points are good.
-/
namespace Bulgaria1998P1
abbrev coloring_is_good {m : ℕ} (color : Set.Icc 1 m → Fin 2) : Prop :=
∃ i j : Set.Icc 1 m,
i < j ∧
∃ h3 : 2 * j.val - i ∈ Set.Icc 1 m,
color i = color j ∧ color i = color ⟨2 * j - i, h3⟩
abbrev all_colorings_are_good (m : ℕ) : Prop :=
3 ≤ m ∧ ∀ color : Set.Icc 1 m → Fin 2, coloring_is_good color
/- determine -/ abbrev solution_value : ℕ := sorry
theorem bulgaria1998_p1 : IsLeast { m | all_colorings_are_good m } solution_value := sorry
```

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: