Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2026P4

import Mathlib.Data.Nat.Digits.Lemmas
import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic

/-!
# USA Mathematical Olympiad 2026, Problem 4

A positive integer n is called solitary if, for any non-negative integers a and b such
that a + b = n, either a or b contains the digit "1".
Determine, with proof, the number of solitary integers less than 10^2026.
-/

namespace Usa2026P4

open Classical

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

def has_digit_one (n : ℕ) : Prop :=
  1 ∈ Nat.digits 10 n

def is_solitary (n : ℕ) : Prop :=
  n > 0 ∧ ∀ a b : ℕ, a + b = n → has_digit_one a ∨ has_digit_one b

theorem usa2026_p4 :
    (Finset.filter is_solitary (Finset.Ico 1 (10^2026))).card = solution := sorry

end Usa2026P4

File author(s): Daniel Liao

This problem does not yet have a complete formalized solution.