lean_workbook_plus_7234

Proved

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

Let $(ax^3-7x^2-10x+24)(2x^5+2x^4+bx^3+5x^2)=2ax^8-2bx^7-24x^6+(b-a)x^5-37x^4+7abx^3+12abx^2$ hold true for all $x$ . Find $a+b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7234 (a b : ℝ) (h : ∀ x : ℝ, (a * x ^ 3 - 7 * x ^ 2 - 10 * x + 24) * (2 * x ^ 5 + 2 * x ^ 4 + b * x ^ 3 + 5 * x ^ 2) = 2 * a * x ^ 8 - 2 * b * x ^ 7 - 24 * x ^ 6 + (b - a) * x ^ 5 - 37 * x ^ 4 + 7 * a * b * x ^ 3 + 12 * a * b * x ^ 2) : a + b = 7   :=  by sorry

Source

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

View graph