lean_workbook_plus_1842

Proved

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

Find $ax^5 + by^5$ if the real numbers $a,b,x$ and $y$ satisfy the equations $ax + by = 3, ~~ ax^2 + by^2 = 7, ~~ ax^3 + by^3 = 16, ~~ ax^4 + by^4 = 42$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1842 (a b x y : ℝ) (h1 : a * x + b * y = 3) (h2 : a * x^2 + b * y^2 = 7) (h3 : a * x^3 + b * y^3 = 16) (h4 : a * x^4 + b * y^4 = 42) : a * x^5 + b * y^5 = 20   :=  by sorry

Source

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

View graph