lean_workbook_plus_72329

Proved

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

Let $a=\frac{1}{2006}$ and $b=\frac{2005}{2006}$ . Then $a^3+b^3+3ab=(a+b)(a^2-ab+b^2)+3ab$ . Since $a+b=1$ , the expression becomes $a^2-ab+b^2+3ab=a^2+2ab+b^2=(a+b)^2=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72329  (a b : ℝ)
  (h₀ : a = 1 / 2006)
  (h₁ : b = 2005 / 2006) :
  a^3 + b^3 + 3 * (a * b) = (a + b) * (a^2 - a * b + b^2) + 3 * (a * b) ∧ a^2 - a * b + b^2 + 3 * (a * b) = a^2 + 2 * a * b + b^2 ∧ a^2 + 2 * a * b + b^2 = (a + b)^2   :=  by sorry

Source

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

View graph