lean_workbook_plus_20761

Disproved

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

Let $z=m^{2} -1$ . \n\n $z( z+1)( z+2)( z+3) =\left( 3m^{2} k^{2} -3mk\right)^{2} +\left( 3mk^{2} +3km^{2}\right)^{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20761 : ∀ m k z : ℂ,  z = m^2 - 1 → z * (z + 1) * (z + 2) * (z + 3) = (3 * m^2 * k^2 - 3 * m * k)^2 + (3 * m * k^2 + 3 * k * m^2)^2   :=  by sorry

Source

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

View graph