Prove2Me

lean_workbook_plus_21312

Disproved

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

Prove that (a−b)(b−c)(c−a)=(b−c)(c−a)+(c−a)(a−b)+(a−b)(b−c)(a-b)(b-c)(c-a) = (b-c)(c-a)+(c-a)(a-b)+(a-b)(b-c).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_21312 : ∀ a b c : ℤ, (a - b) * (b - c) * (c - a) = (b - c) * (c - a) + (c - a) * (a - b) + (a - b) * (b - c)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph