Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2025P2

module

public import Mathlib.Tactic
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Analysis.CStarAlgebra.Classes
public import Mathlib.Analysis.Complex.Polynomial.Basic
public import Mathlib.RingTheory.SimpleRing.Principal

public section


/-!
# USA Mathematical Olympiad 2025, Problem 2

Let `n > k ≥ 1` be integers. Let `P(x) ∈ ℝ[x]` be a polynomial of degree `n` with no
repeated roots and `P(0) ≠ 0`. Suppose that for any real numbers `a₀, a₁, ..., aₖ` such
that the polynomial `aₖxᵏ + ··· + a₁x + a₀` divides `P(x)`, the product `a₀a₁···aₖ` is
zero. Prove that `P(x)` has a nonreal root.
-/

namespace Usa2025P2

open Polynomial Finset

theorem usa2025_p2 (n k : ℕ) (hn : k < n) (hk : 1 ≤ k) (P : ℝ[X])
    (hdeg : P.natDegree = n) (hsq : Squarefree P) (h0 : P.eval 0 ≠ 0)
    (H : ∀ a : Fin (k + 1) → ℝ, (∑ i, C (a i) * X ^ (i : ℕ)) ∣ P → ∏ i, a i = 0) :
    ∃ z : ℂ, aeval z P = 0 ∧ z.im ≠ 0 := sorry

end Usa2025P2

File author(s): Kimi K3

This problem has a complete formalized solution.