lean_workbook_plus_39106

Proved

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

Given for some real $a, b, c, d$ ,\n

P(x) = ax^4 + bx^3 + cx^2 + dx

P(-5) = P(-2) = P(2) = P(5) = 1

\nFind $P(10)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39106 (a b c d : ℝ) (P : ℝ → ℝ) (hP : P = fun x : ℝ => a * x ^ 4 + b * x ^ 3 + c * x ^ 2 + d * x) : P (-5) = 1 ∧ P (-2) = 1 ∧ P 2 = 1 ∧ P 5 = 1 → P 10 = -71   :=  by sorry

Source

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

View graph