lean_workbook_plus_49281

Proved

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

Given $\alpha, \beta$ are real numbers satisfying ${\alpha}^3-3{\alpha}^2+5{\alpha}=1$ and ${\beta}^3-3{\beta}^2+5{\beta}=5$ . Find $\alpha +\beta$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49281 (α β : ℝ) (h₁ : α^3 - 3 * α^2 + 5 * α = 1) (h₂ : β^3 - 3 * β^2 + 5 * β = 5) : α + β = 2   :=  by sorry

Source