Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2019P6

module

public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Analysis.CStarAlgebra.Classes
public import Mathlib.Analysis.Complex.Polynomial.Basic
public import Mathlib.RingTheory.SimpleRing.Principal

public section


/-!
# USA Mathematical Olympiad 2019, Problem 6

Find all polynomials P with real coefficients such that

    P(x)/yz + P(y)/zx + P(z)/xy = P(x − y) + P(y − z) + P(z − x)

for all nonzero real numbers x, y, z obeying 2xyz = x + y + z.
-/

namespace Usa2019P6

open Polynomial

/- determine -/ abbrev SolutionSet : Set (Polynomial ℝ) := sorry

theorem usa2019_p6 (P : Polynomial ℝ) :
    P ∈ SolutionSet ↔
    ∀ x y z : ℝ, x ≠ 0 → y ≠ 0 → z ≠ 0 → 2 * x * y * z = x + y + z →
      P.eval x / (y * z) + P.eval y / (z * x) + P.eval z / (x * y) =
        P.eval (x - y) + P.eval (y - z) + P.eval (z - x) := sorry

end Usa2019P6

File author(s): Kimi K3

This problem has a complete formalized solution.