Prove2Me

lean_workbook_plus_36775

Proved

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

First expand (a+1)(b+1)(c+1)=(a+b+c)+(ab+ac+bc)+abc+1(a + 1)(b + 1)(c + 1) = (a + b + c) + (ab + ac + bc) + abc + 1. By Vieta's formulas, a+b+c=0 a + b + c = 0, ab+ac+bc=−19 ab + ac + bc = - 19, abc=−30 abc = - 30. Plugging in, we have (a+1)(b+1)(c+1)=0+−19+−30+1=−48(a + 1)(b + 1)(c + 1) = 0 + - 19 + - 30 + 1 = \boxed{ - 48}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_36775  (a b c : ℂ)
  (h₀ : a + b + c = 0)
  (h₁ : a * b + b * c + c * a = -19)
  (h₂ : a * b * c = -30) :
  (a + 1) * (b + 1) * (c + 1) = -48   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph