Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2025P1

module

public import Mathlib.Data.List.GetD
public import Mathlib.Data.Nat.Digits.Lemmas

public section


/-!
# USA Mathematical Olympiad 2025, Problem 1

Fix positive integers k and d. Prove that for all sufficiently large odd
positive integers n, the digits of the base-2n representation of n ^ k are
all greater than d.
-/

namespace Usa2025P1

theorem usa2025_p1 (k d : ℕ) (hk : 0 < k) (hd : 0 < d) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → Odd n → ∀ a ∈ Nat.digits (2 * n) (n ^ k), d < a := sorry

end Usa2025P1

File author(s): Kimi K3

This problem has a complete formalized solution.