Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2007P1

module

public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
public import Mathlib.Algebra.Order.Group.Nat
public import Mathlib.Order.Lattice.Nat
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 2007, Problem 1

Let n be a positive integer. Define a sequence by setting a₁ = n and,
for each k > 1, letting aₖ be the unique integer in the range 0 ≤ aₖ ≤ k - 1
for which a₁ + a₂ + ··· + aₖ is divisible by k. (For instance, when n = 9
the obtained sequence is 9, 1, 2, 0, 3, 3, 3, ....)
Prove that for any n the sequence a₁, a₂, ... eventually becomes constant.
-/

namespace Usa2007P1

/-- The partial sums `s n k = a n 0 + a n 1 + ... + a n k` of the sequence of the
problem, defined directly: `s n 0 = n`, and `s n (k + 1)` is the smallest multiple
of `k + 2` which is `≥ s n k`. -/
def s (n : ℕ) : ℕ → ℕ
  | 0 => n
  | (k + 1) => s n k + (k + 2 - s n k % (k + 2)) % (k + 2)

/-- The sequence of the problem, with indices shifted by one so that `a n 0 = n`:
for `k ≥ 1`, `a n k` is the unique integer in `[0, k]` for which `k + 1` divides
`s n k = a n 0 + ... + a n k`. -/
def a (n : ℕ) : ℕ → ℕ
  | 0 => n
  | (k + 1) => s n (k + 1) - s n k

theorem usa2007_p1 (n : ℕ) (hn : 0 < n) :
    ∃ c N, ∀ k ≥ N, a n k = c := sorry

end Usa2007P1

File author(s): Kimi K3

This problem has a complete formalized solution.