## Compfiles: Catalog Of Math Problems Formalized In Lean

## Imo2004P6

```
import Mathlib.Tactic
/-!
# International Mathematical Olympiad 2004, Problem 6
We call a positive integer *alternating* if every two consecutive
digits in its decimal representation are of different parity.
Find all positive integers n such that n has a multiple that is
alternating.
-/
namespace Imo2004P6
/- determine -/ abbrev SolutionSet : Set ℕ := sorry
abbrev Alternating (n : Nat) : Prop :=
(n.digits 10).Chain' (fun k l ↦ ¬ k ≡ l [MOD 2])
theorem imo2004_p6 (n : ℕ) :
n ∈ SolutionSet ↔ 0 < n ∧ ∃ k, Alternating (n * k) := sorry
```

This problem does not yet have a complete formalized solution.

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