Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1975P4

import Mathlib

/-!
# International Mathematical Olympiad 1975, Problem 4

When $4444^{4444}$ is written in decimal notation, the sum of its digits is $A$.
Let $B$ be the sum of the digits of $A$.
Find the sum of the digits of $B$. ($A$ and $B$ are written in decimal notation.)
-/

namespace Imo1975P4

def A : ℕ := (Nat.digits 10 (4444^4444)).sum

def B : ℕ := (Nat.digits 10 A).sum

/- determine -/ abbrev sum_digits_B : ℕ := sorry


theorem imo1975_p4 : sum_digits_B = (Nat.digits 10 B).sum := sorry

end Imo1975P4

File author(s): Constantin Seebach

This problem has a complete formalized solution.