Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2019P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Polynomial.Degree.Lemmas
public import Mathlib.Data.List.TakeWhile
public import Mathlib.Data.Nat.Digits.Lemmas
public import Mathlib.Tactic.NormNum.Prime

public section


/-!
# USA Mathematical Olympiad 2019, Problem 3

Let K be the set of positive integers not containing the decimal digit 7.
Determine all polynomials f(x) with nonnegative coefficients such that
f(x) ∈ K for all x ∈ K.
-/

namespace Usa2019P3

open Polynomial

/-- The set of positive integers whose decimal representation does not
contain the digit 7. -/
def K : Set ℕ := {n | 0 < n ∧ 7 ∉ Nat.digits 10 n}

theorem mem_K {n : ℕ} : n ∈ K ↔ 0 < n ∧ 7 ∉ Nat.digits 10 n := Iff.rfl

/-- The polynomials that map `K` into `K`: the constants with value in `K`,
and the polynomials `10^e * x + k` with `k < 10^e` and `k ∈ K ∪ {0}`. -/
/- determine -/ abbrev solution_set : Set (Polynomial ℕ) := sorry

theorem usa2019_p3 (f : Polynomial ℕ) :
    (∀ n ∈ K, f.eval n ∈ K) ↔ f ∈ solution_set := sorry

end Usa2019P3

File author(s): Kimi K3

This problem has a complete formalized solution.