Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2003P1


import Mathlib.Data.Nat.Digits
import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 2003, Problem 1

Prove that for every positive integer n there exists an n-digit
number divisible by 5ⁿ, all of whose digits are odd.
-/

namespace Usa2003P1

theorem usa2003_p1 (n : ℕ) :
    ∃ m, (Nat.digits 10 m).length = n ∧
          5^n ∣ m ∧ (Nat.digits 10 m).all (Odd ·) := sorry

File author(s): David Renshaw

This problem has a complete formalized solution.

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