lean_workbook_plus_77961

Proved

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

Let numbers are $a, a+1,a+2$ . \nthen: $a^3+(a+1)^3+(a+2)^3=3a^3+9a^2+15a+9$ \nThen: $3a+3|3a^3+9a^2+15a+9$ \nthen: $(3a+3).(a^2+2a+3)=3a^3+9a^2+15a+9$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77961 : ∀ a : ℤ, a^3 + (a + 1)^3 + (a + 2)^3 = 3 * a^3 + 9 * a^2 + 15 * a + 9 ∧ 3 * a + 3 ∣ 3 * a^3 + 9 * a^2 + 15 * a + 9 ∧ (3 * a + 3) * (a^2 + 2 * a + 3) = 3 * a^3 + 9 * a^2 + 15 * a + 9 ∧ a^2 + 2 * a + 3 = a^2 + 2 * a + 3 ∧ (3 * a + 3) * (a^2 + 2 * a + 3) = 3 * a^3 + 9 * a^2 + 15 * a + 9   :=  by sorry

Source

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

View graph