lean_workbook_plus_78403

Proved

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

Let $a = (2 + \sqrt{5})^{2n}$ and $b = (2 - \sqrt{5})^{2n}$ . The above expression reduces to $\frac{a^3 + b^3}{a + b} = a^2 - ab + b^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78403 (a b : ℝ) (n : ℕ) : a = (2 + Real.sqrt 5)^(2 * n) ∧ b = (2 - Real.sqrt 5)^(2 * n) → (a^3 + b^3) / (a + b) = a^2 - a * b + b^2   :=  by sorry

Source

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

View graph