lean_workbook_plus_48481

Proved

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

Let $p(x)=x^4+ax^3+bx^2+cx+d$ where a,b,c,d are constant, $p(1)=1993, p(2)=3986, p(3)=5979$ ,find the value of : $\frac{1}{4}[p(11)+p(-7)]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48481 (a b c d : ℝ) (p : ℝ → ℝ) (hp : p = fun x : ℝ => x^4 + a*x^3 + b*x^2 + c*x + d) : p 1 = 1993 ∧ p 2 = 3986 ∧ p 3 = 5979 → 1/4 * (p 11 + p (-7)) = 5233   :=  by sorry

Source

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

View graph