import Mathlib.Tactic
/-!
# International Mathematical Olympiad 1976, Problem 6
The sequence u_0, u_1, u_2, ... is defined by:
u_0 = 2, u_1 = 5/2, u_{n+1} = u_n(u_{n-1}^2 - 2) - u_1 for n = 1, 2, ... .
Prove that ⌊u_n⌋ = 2^(2^n - (-1)^n)/3 for all positive n,
where ⌊x⌋ denotes the greatest integer less than or equal to x.
-/
namespace Imo1976P6
theorem imo1976_p6 (u : ℕ → ℝ)
(h₀ : u 0 = 2)
(h₁ : u 1 = 5 / 2)
(h₂ : ∀ n, u (n + 2) = u (n + 1) * ((u n) ^ 2 - 2) - u 1) :
∀ n > 0, ⌊u n⌋ = (2 : ℝ) ^ ((2^n - (-1 : ℝ) ^ n) / 3) := sorry
end Imo1976P6
This problem has a complete formalized solution.