Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1996P3


import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1996, Problem 3

Let S denote the set of nonnegative integers. Find
all functions f from S to itself such that

 f(m + f(n)) = f(f(m)) + f(n)

for all m,n in S.
-/

namespace Imo1996P3

/- determine -/ abbrev SolutionSet : Set (ℕ → ℕ) := sorry

theorem imo1996_p3 (f : ℕ → ℕ) :
    f ∈ SolutionSet ↔ ∀ m n, f (m + f n) = f (f m) + f n := sorry

This problem does not yet have a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org:
External resources: