lean_workbook_plus_63888

Proved

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

For some constant $k$ the polynomial $p(x) = 3x^2 + kx + 117$ has the property that $p(1) = p(10)$ . Evaluate $p(20)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63888 (p : ℝ → ℝ) (k : ℝ) (h₁ : p = fun x : ℝ => 3 * x^2 + k * x + 117) (h₂ : p 1 = p 10) : p 20 = 657   :=  by sorry

Source