lean_workbook_plus_68404

Proved

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

Solve for $x^5 + y^5$ where $x$ and $y$ are real numbers that satisfy $x+y=3$ and $xy=2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68404 (x y : ℝ) (h₁ : x + y = 3) (h₂ : x * y = 2) : x^5 + y^5 = 33   :=  by sorry

Source