Prove2Me

lean_workbook_plus_56308

Proved

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

And use Titu Lemma: \n

(abc+bcd+cda+dab)23(abc+bcd+cda+dab)=abc+bcd+cda+dab3\frac{(abc+bcd+cda+dab)^2}{3(abc+bcd+cda+dab)}=\frac{abc+bcd+cda+dab}{3}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_56308 (a b c d : ℝ) : (a * b * c + b * c * d + c * d * a + d * a * b) ^ 2 / (3 * (a * b * c + b * c * d + c * d * a + d * a * b)) = (a * b * c + b * c * d + c * d * a + d * a * b) / 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph