Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2012P4

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2012, Problem 4

Determine all functions f : ℤ → ℤ such that for all integers a,b,c with a + b + c = 0,
the following equality holds:
  f(a)² + f(b)² + f(c)² = 2f(a)f(b) + 2f(b)f(c) + 2f(c)f(a).
-/

namespace Imo2012P4

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

theorem imo2012_p4 (f : ℤ → ℤ) :
    f ∈ solution_set ↔
    ∀ a b c : ℤ, a + b + c = 0 →
      (f a)^2 + (f b)^2 + (f c)^2 =
        2 * f a * f b + 2 * f b * f c + 2 * f c * f a := sorry

end Imo2012P4

File author(s): spinylobster, ondanaoto, Seasawher

This problem has a complete formalized solution.