Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1974P6

module

public import Mathlib.Tactic
public import Mathlib.Algebra.Polynomial.Roots

public section


/-!
# International Mathematical Olympiad 1974, Problem 6

Let $P$ be a non-constant polynomial with integer coefficients. If $n(P)$ is
the number of different integers $k$ such that $(P(k))^2 = 1$, prove that
$n(P) - \deg(P) \leq 2$.

We formalize $n(P)$ as the cardinality (`Set.ncard`) of the set of integers
`k` with `P.eval k ^ 2 = 1`, and prove the equivalent inequality
`n(P) ≤ deg(P) + 2`.
-/

namespace Imo1974P6

open Polynomial

theorem imo1974_p6 (P : Polynomial ℤ) (hP : 0 < P.natDegree) :
    {k : ℤ | P.eval k ^ 2 = 1}.ncard ≤ P.natDegree + 2 := sorry

end Imo1974P6

File author(s): Kimi K3

This problem has a complete formalized solution.