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
This problem does not yet have a complete formalized solution.