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 computation are strictly prohibited >:(_

Replace sorry in the template below with your solution. See Answer Bank for acceptible answer declarations. Mathlib version used by the checker is v4.29.0.

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