lean_workbook_plus_73446

Proved

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

For real numbers a,b,c,d, the polynomial p(x) has the form of: $p(x)=x^4+ax^3+bx^2+cx+d$ That satisfies: $p(1)=827$ $p(2)=1654$ $p(3)=2481$ Find the value of $\frac{p(9)+p(-5)}{4}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73446 (a b c d : ℝ) (p : ℝ → ℝ) (hp : p = fun x : ℝ => x^4 + a*x^3 + b*x^2 + c*x + d) : p 1 = 827 ∧ p 2 = 1654 ∧ p 3 = 2481 → (p 9 + p (-5)) / 4 = 2003   :=  by sorry

Source

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

View graph