lean_workbook_plus_3904

Proved

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

Let $f(a)=a^2(x)+(a+1)^2(y)+(a+2)^2(z)$ .\nWe have $f(1)=305$ , $f(2)=319$ , $f(3)=880$ .\nClearly, $f(a)$ is degree 2.\nWe apply finite differences.\nWe have first differences of $14,561$ and the second difference is $547$ .\n $f(4)=880+561+547=880+1108=\boxed{1988}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3904  (x y z : ℝ)
  (f : ℕ → ℝ)
  (h₀ : ∀ a, f a = a^2 * x + (a + 1)^2 * y + (a + 2)^2 * z)
  (h₁ : f 1 = 305)
  (h₂ : f 2 = 319)
  (h₃ : f 3 = 880) :
  f 4 = 1988   :=  by sorry

Source

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

View graph