lean_workbook_plus_64302

Proved

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

let $P(x,y)$ be the assersion,

f(x+y)=x+f(y).

Then, $P(x,0)$ yields, $f(x)=x+f(0)=x+2.$ for all real numbers $x.$ \nTherefore, $f(1998)=1998+2=2000.$ Which corresponds to answer choice $\textbf{(E)}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64302  (f : ℝ → ℝ)
  (h₀ : ∀ x, ∀ y, f (x + y) = x + f y)
  (h₁ : f 0 = 2) :
  f 1998 = 2000   :=  by sorry

Source

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

View graph