Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2022P3

import Mathlib.Data.Real.Basic
import Mathlib.Data.NNReal.Basic
import Mathlib.Algebra.Order.Positive.Field
import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 2022, Problem 3

Let ℝ+ be the set of all positive real numbers. Find all
functions ℝ+ → ℝ+ such that for all x, y ∈ ℝ+ we have

   f(x) = f(f(f(x)) + y) + f(xf(y))f(x+y).
-/

namespace Usa2022P3

abbrev PosReal : Type := { x : ℝ // 0 < x }
notation "ℝ+" => PosReal

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

theorem usa2022_p3 (f : ℝ+ → ℝ+) :
  f ∈ solution_set ↔
    (∀ x y : ℝ+, f x = f (f (f x) + y) + f (x * f y) * f (x + y)) := sorry


end Usa2022P3

File author(s): Zhiyi Luo

This problem has a complete formalized solution.