Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2002P4

import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 2002, Problem 4

Find all functions f : ℝ → ℝ such that for all x, y ∈ ℝ:
f(x² - y²) = x f(x) - y f(y).
-/

namespace Usa2002P4

def FE (f : ℝ → ℝ) : Prop :=
  ∀ x y, f (x^2 - y^2) = x * (f x) - y * (f y)

/- determine -/ abbrev solution_set : Set (ℝ → ℝ) := sorry

theorem usa2002_p4 (f : ℝ → ℝ) :
    f ∈ solution_set ↔ FE f := sorry

end Usa2002P4

File author(s): Evan Chen

This problem has a complete formalized solution.