Prove2Me

lean_workbook_plus_29879

Proved

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

WLOG a+b+c=9,ab+bc+ca=24 a+b+c=9,ab+bc+ca=24 . Let a−1=x,b−1=y,c−1=z a-1=x,b-1=y,c-1=z and a−2=p,b−2=q,c−2=r a-2=p,b-2=q,c-2=r . So x+y+z=6,xy+yz+zx=9 x+y+z=6,xy+yz+zx=9 , p+q+r=3,pq+qr+rp=0 p+q+r=3,pq+qr+rp=0 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_29879 {a b c x y z p q r : ℝ} (ha : a + b + c = 9) (hb : a * b + b * c + c * a = 24) (hx : x = a - 1) (hy : y = b - 1) (hz : z = c - 1) (hp : p = a - 2) (hq : q = b - 2) (hr : r = c - 2) : x + y + z = 6 ∧ x * y + y * z + z * x = 9 ∧ p + q + r = 3 ∧ p * q + q * r + r * p = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph