← Formalpedia
lean_workbook_plus_82188 Disproved by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
proofwiki
Thus: ( 3 a − b − c ) ( b − c ) 2 + ( 3 b − c − a ) ( c − a ) 2 + ( 3 c − a − b ) ( a − b ) 2 ≥ ( 3 a − b − c + 3 b − c − a ) ( b − c ) 2 + ( 3 c − a − b + 3 b − c − a ) ( a − b ) 2 ≥ 0 (3a - b - c)(b - c)^2 + (3b - c - a)(c - a)^2 + (3c - a - b)(a - b)^2 \ge (3a - b - c + 3b - c - a)(b - c)^2 + (3c - a - b + 3b - c - a)(a - b)^2 \ge 0 ( 3 a − b − c ) ( b − c ) 2 + ( 3 b − c − a ) ( c − a ) 2 + ( 3 c − a − b ) ( a − b ) 2 ≥ ( 3 a − b − c + 3 b − c − a ) ( b − c ) 2 + ( 3 c − a − b + 3 b − c − a ) ( a − b ) 2 ≥ 0 ⟺ \iff ⟺ 2 ( a + b − c ) ( b − c ) 2 + 2 ( b + c − a ) ( a − b ) 2 ≥ 0 2(a + b - c)(b - c)^2 + 2(b + c - a)(a - b)^2 \ge 0 2 ( a + b − c ) ( b − c ) 2 + 2 ( b + c − a ) ( a − b ) 2 ≥ 0
Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_82188 :
∀ a b c : ℝ,
(3 * a - b - c) * (b - c) ^ 2 + (3 * b - c - a) * (c - a) ^ 2 + (3 * c - a - b) * (a - b) ^ 2 ≥ 0 := by sorry View graph