Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2024P3

import Mathlib.Tactic
import Mathlib.Data.Set.Card
import Mathlib.Data.Nat.Nth

/-!
# International Mathematical Olympiad 2024, Problem 3

Let a₁, a₂, a₃, ... be an infinite sequence of positive integers,
and let N be a positive integer. Suppose that, for each n > N,
aₙ is equal to the number of times aₙ₋₁ appears in the list
a₁, a₂, ..., aₙ₋₁.

Prove that at least one of the sequences a₁, a₃, a₅, ... and
a₂, a₄, a₆, ... is eventually periodic.
-/

namespace Imo2024P3

open scoped Finset

def Condition (a : ℕ → ℕ) (N : ℕ) : Prop :=
  (∀ i, 0 < a i) ∧ ∀ n, N < n → a n = #{i ∈ Finset.range n | a i = a (n - 1)}

def EventuallyPeriodic (b : ℕ → ℕ) : Prop :=
  ∃ p M, 0 < p ∧ ∀ m, M ≤ m → b (m + p) = b m

theorem imo2024_p3 {a : ℕ → ℕ} {N : ℕ} (h : Condition a N) :
    EventuallyPeriodic (fun i ↦ a (2 * i)) ∨ EventuallyPeriodic (fun i ↦ a (2 * i + 1)) := sorry

end Imo2024P3

File author(s): Joseph Myers

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo2024Q3.lean.