Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1992P5

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Analysis.Complex.Polynomial.Basic
public import Mathlib.RingTheory.SimpleRing.Principal

public section


/-!
# USA Mathematical Olympiad 1992, Problem 5

A complex polynomial has degree 1992 and distinct zeros. Show that we can find
complex numbers zₙ, such that if p₁(z) = z - z₁ and pₙ(z) = pₙ₋₁(z)² - zₙ,
then the polynomial divides p₁₉₉₂(z).
-/

namespace Usa1992P5

open Polynomial

/-- The iterated polynomial sequence of the problem: `pseq [z₁, …, zₙ]` is the
polynomial `pₙ`, where `p₁(z) = z - z₁` and `pₖ(z) = pₖ₋₁(z)² - zₖ`. -/
noncomputable def pseq : List ℂ → ℂ[X]
  | [] => X
  | z :: zs => zs.foldl (fun P w => P ^ 2 - C w) (X - C z)

theorem usa1992_p5 {q : ℂ[X]} (hq : q.natDegree = 1992) (hq' : q.roots.Nodup) :
    ∃ zs : List ℂ, zs.length = 1992 ∧ q ∣ pseq zs := sorry

end Usa1992P5

File author(s): Kimi K3

This problem has a complete formalized solution.