lean_workbook_plus_25724

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Does there exist a function $f:\mathbb{N}\to\mathbb{N}$ such that $f(2008)\not= 2008$ and $f(m+f(n))=f(f(m))+f(n)$ for all $m,n\in\mathbb{N}$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25724 : ∃ f : ℕ → ℕ, f 2008 ≠ 2008 ∧ ∀ m n, f (m + f n) = f (f m) + f n   :=  by sorry

Source