Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1992P1

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

/-!
# USA Mathematical Olympiad 1992, Problem 1

Find, as a function of n, the sum of the digits of

     9 × 99 × 9999 × ... × (10^2ⁿ - 1),

where each factor has twice as many digits as the last one.
-/

namespace Usa1992P1

/- determine -/ abbrev solution : ℕ → ℕ := sorry

theorem usa1992_p1 (n : ℕ) :
    (Nat.digits 10
     (∏ i ∈ Finset.range (n + 1), (10^(2^i) - 1))).sum = solution n := sorry

end Usa1992P1

File author(s): David Renshaw

This problem has a complete formalized solution.