Prove2Me

lean_workbook_plus_18282

Proved

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

The real numbers α,β\alpha ,\beta satisfy the equations

α3−3α2+5α−17=0\alpha^3-3\alpha^2+5\alpha-17=0 β3−3β2+5β+11=0\beta^3-3\beta^2+5\beta+11=0

Find α+β\alpha+\beta .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18282 (α β : ℝ) (h₁ : α^3 - 3 * α^2 + 5 * α - 17 = 0) (h₂ : β^3 - 3 * β^2 + 5 * β + 11 = 0) : α + β = 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph