by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
prove f(a,b,c)≥0, where f(a,b,c)=12a6+31a5b+4a5c−38a4b2+9a4bc+16a4c2−33a3b3−20a3b2c+61a3bc2−33a3c3+16a2b4+61a2b3c−126a2b2c2−20a2bc3−38a2c4+4ab5+9ab4c−20ab3c2+61ab2c3+9abc4+31ac5+12b6+31b5c−38b4c2−33b3c3+16b2c4+4bc5+12c6
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27939 : ∀ a b c : ℝ, 12 * a ^ 6 + 31 * a ^ 5 * b + 4 * a ^ 5 * c - 38 * a ^ 4 * b ^ 2 + 9 * a ^ 4 * b * c + 16 * a ^ 4 * c ^ 2 - 33 * a ^ 3 * b ^ 3 - 20 * a ^ 3 * b ^ 2 * c + 61 * a ^ 3 * b * c ^ 2 - 33 * a ^ 3 * c ^ 3 + 16 * a ^ 2 * b ^ 4 + 61 * a ^ 2 * b ^ 3 * c - 126 * a ^ 2 * b ^ 2 * c ^ 2 - 20 * a ^ 2 * b * c ^ 3 - 38 * a ^ 2 * c ^ 4 + 4 * a * b ^ 5 + 9 * a * b ^ 4 * c - 20 * a * b ^ 3 * c ^ 2 + 61 * a * b ^ 2 * c ^ 3 + 9 * a * b * c ^ 4 + 31 * a * c ^ 5 + 12 * b ^ 6 + 31 * b ^ 5 * c - 38 * b ^ 4 * c ^ 2 - 33 * b ^ 3 * c ^ 3 + 16 * b ^ 2 * c ^ 4 + 4 * b * c ^ 5 + 12 * c ^ 6 ≥ 0 := by sorry