Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1974P1

import Mathlib.Data.Int.Basic
import Mathlib.Algebra.Polynomial.Div

/-!
# USA Mathematical Olympiad 1974, Problem 1

Let a, b, c be three distinct integers, and let P be a polynomial
with integer coefficients. Show that in this case the conditions
P (a) = b, P (b) = c, P (c) = a cannot be satisfied simultaneously.
-/

open Int

open Polynomial

namespace Usa1974P1

theorem usa1974_p1 {P : Polynomial ℤ} (a b c : ℤ) (h_neq : a ≠ b ∧ b ≠ c ∧ c ≠ a) :
  ¬(P.eval a = b ∧ P.eval b = c ∧ P.eval c = a) := sorry

end Usa1974P1

File author(s): Maximiliano Onofre Martínez

This problem has a complete formalized solution.