Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1990P4

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Nat.Digits.Lemmas
public import Mathlib.Data.Set.Card
public import Mathlib.Order.CompletePartialOrder

public section


/-!
# USA Mathematical Olympiad 1990, Problem 4

How many positive integers can be written in base n so that
(1) the integer has no two digits the same, and
(2) each digit after the first differs by one from an earlier digit?
For example, in base 3, the possible numbers are 1, 2, 10, 12, 21, 102, 120, 210.
-/

namespace Usa1990P4

/-- Condition (2) of the problem, phrased for the list of base-`n` digits of a
number as produced by `Nat.digits` (least significant digit first, so the
"first" digit of the number is the last entry of the list): every digit except
the most significant one differs by one from some more significant digit. -/
def DiffByOne (l : List ℕ) : Prop :=
  ∀ i, ∀ (_ : i + 1 < l.length), ∃ j, i < j ∧ j < l.length ∧ ∀ (_ : j < l.length),
    (l[i] + 1 = l[j] ∨ l[j] + 1 = l[i])

/- determine -/ abbrev answer (n : ℕ) : ℕ := sorry

theorem usa1990_p4 (n : ℕ) (hn : 2 ≤ n) :
    Set.ncard {m : ℕ | 0 < m ∧ (Nat.digits n m).Nodup ∧ DiffByOne (Nat.digits n m)} =
      answer n := sorry

end Usa1990P4

File author(s): Kimi K3

This problem has a complete formalized solution.