Prove2Me

lean_workbook_plus_35806

Proved

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

Find all the function f ⁣:Z→Zf\colon \mathbb{Z}\to\mathbb{Z} satisfying the following conditions\n1) f(f(m−n))=f(m2)+f(n)−2nf(m)f(f(m-n))=f(m^2)+f(n)-2nf(m) for all m,n∈Zm,n{\in}Z . 2) f(1)>0f(1)>0 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35806 (f : ℤ → ℤ) (hf: f 1 > 0) (hf2: ∀ m n:ℤ, f (f (m - n)) = f (m^2) + f n - 2 * n * f m): ∀ x:ℤ, f x = x + 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph