## 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, u1 = 5/2, u_{n+1} = un(u_{n-1}^2 - 2) - u_1 for n = 1, 2, ... .
Prove that \[un\] = 2^(2^n - (-1)^n)/3, 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, ⌊u n⌋ = (2:ℝ) ^((2^n - (-1 : ℝ)^n) / 3):= sorry
end Imo1976P6
```

File author(s): InternLM-MATH LEAN Formalizer v0.1

This problem does not yet have a complete formalized solution.

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