Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2006P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Analysis.Normed.Field.Lemmas
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Rat.Star
public import Mathlib.RingTheory.Int.Basic
public import Mathlib.RingTheory.Polynomial.GaussLemma

public section


/-!
# USA Mathematical Olympiad 2006, Problem 3

For integral m, let p(m) be the greatest prime divisor of m. By convention,
we set p(±1) = 1 and p(0) = ∞. Find all polynomials f with integer
coefficients such that the sequence

    {p(f(n²)) − 2n},  n = 0, 1, 2, ...

is bounded above. (In particular, this requires f(n²) ≠ 0 for n ≥ 0.)
-/

namespace Usa2006P3

open Polynomial

theorem usa2006_p3 (f : ℤ[X]) : BddCond f ↔ Classification f := sorry

end Usa2006P3

File author(s): Kimi K3

This problem has a complete formalized solution.