lean_workbook_plus_1896

Proved

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

Find all functions $f: \mathbb{N} \rightarrow \mathbb{N}$ such that $f(m + n) = f(m) + f(n) + mn$ for all positive integers $m$ and $n$ , and $f(1) = 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1896 (f : ℕ → ℕ) (hf: f 1 = 1) (hf1: ∀ m n: ℕ, f (m + n) = f m + f n + m * n): ∀ n:ℕ, f n = n * (n + 1) / 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph