Prove2Me

lean_workbook_plus_65807

Disproved

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

Prove a4/4+(a3b)/4+(a3c)/4+a2bc/4+(ab3)/4+ab2c/4+abc2/4+(ac3)/4+b4/4+(b3c)/4+(bc3)/4+c4/4≥0a^4/4+(a^3 b)/4+(a^3 c)/4+a^2 b c/4+(a b^3)/4+a b^2 c/4+a b c^2/4+(a c^3)/4+b^4/4+(b^3 c)/4+(b c^3)/4+c^4/4\ge 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65807 : ∀ a b c : ℝ, a^4/4 + a^3 * b / 4 + a^3 * c / 4 + a^2 * b * c / 4 + a * b^3 / 4 + a * b^2 * c / 4 + a * b * c^2 / 4 + a * c^3 / 4 + b^4 / 4 + b^3 * c / 4 + b * c^3 / 4 + c^4 / 4 ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph