Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1976P6

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

File author(s): InternLM-MATH LEAN Formalizer v0.1, Aristotle-Harmonic, David Renshaw

This problem has a complete formalized solution.