Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1976P2

import Mathlib

/-!
# International Mathematical Olympiad 1976, Problem 2

Let $P_{1}(x) = x^{2} - 2$ and $P_{j}(x) = P_{1}(P_{j - 1}(x))$ for $j= 2,\ldots$.
Show that for any positive integer $n,$ the roots of the equation $P_{n}(x) = x$ are real and distinct.
-/

namespace Imo1976P2

open Polynomial

noncomputable def P (j : ℕ) : ℝ[X] :=
  match j with
  | 0 => 0
  | 1 => X^2 - 2
  | j+2 => (P 1).comp (P (j+1))


theorem imo1976_p2 (n : ℕ) (npos : 0 < n) :
    (∀ (r : ℂ), r ∈ aroots (P n - X) ℂ → r.im = 0) ∧ (aroots (P n - X) ℂ).Nodup := sorry

end Imo1976P2

File author(s): Constantin Seebach

This problem has a complete formalized solution.