Italy February Round 2025 Problem 4

Let $n$ be a positive integer. Define $f(n)$ as the sum of the digits of $n$ plus the product of the digits of $n$. For example, $f(143) = 1 + 4 + 3 + 1 \cdot 4 \cdot 3$. How many three-digit positive integers $m$ satisfy $$f(m) = f(m-1) + 25?$$

Note: Solutions by direct computation are strictly prohibited >:(

import Mathlib.Data.Nat.Digits.Defs
import Mathlib.Order.Interval.Finset.Defs
import Mathlib.Order.Interval.Finset.Nat

def answer : ℕ := sorry

def f (n : ℕ) : ℕ := (Nat.digits 10 n).sum + (Nat.digits 10 n).prod

theorem solution : {m ∈ Finset.Icc 100 999 | f m = f (m - 1) + 25}.card = answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions