```
import Mathlib.Tactic
/-!
# International Mathematical Olympiad 2018, Problem 5
Let a₁, a₂, ... be an infinite sequence of positive integers.
Suppose that there is an integer N > 1 such that for each n ≥ N
the number
a₁/a₂ + a₂/a₃ ... + aₙ₋₁/aₙ + aₙ/a₁
is an integer. Prove that there is a positive integer M such that
aₘ = aₘ₊₁ for all m ≥ M.
-/
namespace Imo2018P5
theorem imo2018_p5
(a : ℕ → ℤ)
(apos : ∀ n, 0 < a n)
(N : ℕ)
(hN : 0 < N)
(h : ∀ n, N ≤ n →
∃ z : ℤ,
z = ∑ i in Finset.range n, (a i : ℚ) / a ((i + 1) % n))
: ∃ M, ∀ m, M ≤ m → a m = a (m + 1) := sorry
end Imo2018P5
```

This problem does not yet have a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org:

External resources: