Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2014P2

import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 2014, Problem 2

Let ℤ be the set of integers. Find all functions f : ℤ → ℤ such that
x * f(2 * f(y) - x) + y ^ 2 * f(2 * x - f(y)) = (f(x) ^ 2) / x + f(y * f(y))
for all x, y ∈ ℤ with x ≠ 0.
-/

namespace Usa2014P2

def P (f : ℤ → ℤ) :=
    ∀ x y, x ≠ 0 → x * f (2 * f y - x) + y ^ 2 * f (2 * x - f y) = (f x ^ 2 : ℚ) / x + f (y * f y)

/- determine -/ abbrev S : Set (ℤ → ℤ) := sorry

theorem usa2014_p2 {f : ℤ → ℤ} : P f ↔ f ∈ S := sorry

end Usa2014P2

File author(s): Ansar Azhdarov

This problem has a complete formalized solution.