lean_workbook_plus_8603

Proved

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

Given a quadratic polynomial $ax^2+bx+c$ , prove that the third finite difference $f(x+3)-3f(x+2)+3f(x+1)-f(x)$ vanishes.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8603 (a b c : ℝ) (f : ℝ → ℝ) (h : ∀ x, f x = a * x ^ 2 + b * x + c) : ∀ x, f (x + 3) - 3 * f (x + 2) + 3 * f (x + 1) - f x = 0   :=  by sorry

Source

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

View graph