Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2017P1

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2017, Problem 1

For any integer a₀ > 1, define the sequence

  aₙ₊₁ =   √aₙ, if aₙ is a perfect square
        or aₙ + 3 otherwise.

Find all values of a₀ for which there exists A such that aₙ = A for
infinitely many values of n.
-/

namespace Imo2017P1


/- determine -/ abbrev solution_set : Set ℕ := sorry


theorem imo2017_p1
  (a : ℕ → ℕ → ℕ)
  (ha₀: ∀ x, a x 0 = x)
  (ha₁: ∀ x i, 1 < x → if IsSquare (a x i)
                       then a x (i + 1) = Nat.sqrt (a x i)
                       else a x (i + 1) = a x i + 3) :
  ∀ x > 1, (∃ A, {n | a x n = A}.Infinite) ↔ x ∈ solution_set := sorry


end Imo2017P1

File author(s): Roozbeh Yousefzadeh, David Renshaw

This problem has a complete formalized solution.

The solution was imported from IMO-Steps/Lean_v20/imo_proofs/imo_2017_p1.lean.