lean_workbook_plus_6948

Proved

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

For 4th power polynomial $P(x)$ we're given: $P(2) = P(1) = P(-1) = -2$ and $P(-2) = P(3) = 14$ . Then find $P(0).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6948 (a b c d e f : ℝ) (h₁ : a*2^4 + b*2^3 + c*2^2 + d*2 + e = -2) (h₂ : a + b + c + d + e = -2) (h₃ : a*(-1)^4 + b*(-1)^3 + c*(-1)^2 + d*(-1) + e = -2) (h₄ : a*(-2)^4 + b*(-2)^3 + c*(-2)^2 + d*(-2) + e = 14) (h₅ : a*3^4 + b*3^3 + c*3^2 + d*3 + e = 14) : a*0^4 + b*0^3 + c*0^2 + d*0 + e = -2   :=  by sorry

Source

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

View graph