lean_workbook_plus_12893

Proved

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

prove that $3(a^{2}+b^{2}+c^{2}+d^{2})\geq 2(ab+ac+ad+bc+bd+cd)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12893 : ∀ a b c d : ℝ, 3 * (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) ≥ 2 * (a * b + a * c + a * d + b * c + b * d + c * d)   :=  by sorry

Source

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

View graph