Prove2Me

lean_workbook_plus_43787

Proved

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

f(x+y)+f(x−y)=(x+y)22+(x−y)22=x2+2xy+y22+x2−2xy+y22=x2+y2f(x+y)+f(x-y)=\frac{(x+y)^2}{2}+\frac{(x-y)^2}{2}=\frac{x^2+2xy+y^2}{2}+\frac{x^2-2xy+y^2}{2}=x^2+y^2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43787  (x y : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = x^2 / 2)
  (h₁ : ∀ x, ∀ y, f (x + y) + f (x - y) = (x + y)^2 / 2 + (x - y)^2 / 2) :
  f (x + y) + f (x - y) = x^2 + y^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph