Prove2Me

lean_workbook_plus_52052

Proved

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

Find p(p−1)(p−8)+q(q−1)(q−8)+r(r−1)(r−8) p(p - 1)(p - 8) + q(q - 1)(q - 8) + r(r - 1)(r - 8) given the equation x3−9x2+8x+2=0 x^3 - 9x^2 + 8x + 2 = 0 with roots p p , q q , r r .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52052 (p q r : ℂ) (hp : p^3 - 9 * p^2 + 8 * p + 2 = 0) (hq : q^3 - 9 * q^2 + 8 * q + 2 = 0) (hr : r^3 - 9 * r^2 + 8 * r + 2 = 0) : p * (p - 1) * (p - 8) + q * (q - 1) * (q - 8) + r * (r - 1) * (r - 8) = -6   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph