lean_workbook_plus_16973

Proved

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

Determine $ax ^ 5 + by ^ 5$ if the real numbers a, b, x and y satisfy the equations $ax + by = 1, ax ^ 2 + by ^ 2 = 2, ax ^ 3 + by ^ 3 = 5, ax ^ 4 + by ^ 4 = 6$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16973 (a b x y : ℝ) (h₁ : a * x + b * y = 1) (h₂ : a * x ^ 2 + b * y ^ 2 = 2) (h₃ : a * x ^ 3 + b * y ^ 3 = 5) (h₄ : a * x ^ 4 + b * y ^ 4 = 6) : a * x ^ 5 + b * y ^ 5 = 41   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph