lean_workbook_plus_67990

Proved

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

Prove that the inequality is true for any real numbers \n\n $a^2b^2 + a^2c^2 + b^2c^2 >= a^2bc + ab^2c + abc^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67990 (a b c: ℝ) : a ^ 2 * b ^ 2 + a ^ 2 * c ^ 2 + b ^ 2 * c ^ 2 >= a ^ 2 * b * c + a * b ^ 2 * c + a * b * c ^ 2   :=  by sorry

Source

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

View graph