Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1993P1

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1993, Problem 1

Let $f\left(x\right)=x^n+5x^{n-1}+3$, where $n>1$ is an integer.
Prove that $f\left(x\right)$ cannot be expressed as the product of two non-constant polynomials with integer coefficients.
-/

namespace Imo1993P1

open Polynomial

noncomputable def f (n : ℕ) : ℤ[X] := X^n + 5*X^(n-1) + 3

def isConstant {R : Type*} [Semiring R] (p : R[X]) : Prop := ∀ i > 0, p.coeff i = 0

theorem imo1993_p1 : ∀ n > 1, ¬∃ p q : ℤ[X], f n = p*q ∧ ¬ isConstant p ∧ ¬ isConstant q := sorry


end Imo1993P1

File author(s): Constantin Seebach

This problem has a complete formalized solution.