lean_workbook_plus_8439

Proved

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

Hence $f(m+1,1)=f(m,1)+m+1$ .Now $P(1,1)\implies f(1,1)=1$ , and an easy induction gives $f(k,1)=k(k+1)/2$ for all positive integers $k$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8439  (m : ℕ)
  (f : ℕ → ℕ)
  (h₀ : ∀ m, f (m + 1) = f m + m + 1)
  (h₁ : f 1 = 1) :
  f m = m * (m + 1) / 2   :=  by sorry

Source

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

View graph