Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1995P1

module

public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Data.List.GetD
public import Mathlib.NumberTheory.Padics.PadicVal.Basic

public section


/-!
# USA Mathematical Olympiad 1995, Problem 1

Let `p` be an odd prime. The sequence `(aₙ) n ≥ 0` is defined as follows:
`a₀ = 0, a₁ = 1, ..., a_{p-2} = p - 2`, and for all `n ≥ p - 1`, `aₙ` is the
least integer greater than `a_{n-1}` such that `a₀, a₁, ..., aₙ` does not
contain an arithmetic progression of length `p`.

Prove that, for all `n`, `aₙ` is the number obtained by writing `n` in base
`p - 1` and reading the result in base `p`.
-/

namespace Usa1995P1

/-- `HasAp a p n m` means that the first `n + 1` terms `a 0, a 1, …, a (n-1), m`
(where the candidate `m` is the `n`-th term) contain an arithmetic progression
of length `p`: there are strictly increasing indices `v 0 < v 1 < … < v (p-1)`,
all at most `n`, whose values form an arithmetic progression. The last
conjunct splits the value condition according to whether the index is the
final position `n` (where the candidate `m` sits) or not. -/
def HasAp (a : ℕ → ℕ) (p n m : ℕ) : Prop :=
  ∃ v : Fin p → ℕ, StrictMono v ∧ (∀ i, v i ≤ n) ∧
    ∃ x d : ℕ, ∀ i : Fin p, (v i < n → a (v i) = x + i.val * d) ∧
      (v i = n → m = x + i.val * d)

/-- USA Mathematical Olympiad 1995, Problem 1. -/
theorem usa1995_p1 (p : ℕ) (hp : p.Prime) (ho : Odd p) (a : ℕ → ℕ)
    (ha₀ : ∀ n < p - 1, a n = n)
    (ha₁ : ∀ n ≥ p - 1, IsLeast {m | a (n - 1) < m ∧ ¬ HasAp a p n m} (a n)) :
    ∀ n, a n = Nat.ofDigits p (Nat.digits (p - 1) n) := sorry

end Usa1995P1

File author(s): Kimi K3

This problem has a complete formalized solution.