Prove2Me

lean_workbook_plus_16894

Proved

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

Prove the equivalence of the following conditions for a symmetric polynomial of degree 3, P(a,b,c)P(a, b, c): \n1) P(1,1,1),P(1,1,0),P(1,0,0)≥0.P(1, 1, 1), P(1, 1, 0), P(1, 0, 0) \geq 0. \n2) P(a,b,c)≥0,∀a,b,c≥0.P(a, b, c) \geq 0, \forall a, b, c \geq 0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16894 (P : ℝ → ℝ → ℝ → ℝ) (h : P = fun a b c ↦ a^3 + b^3 + c^3 - 3*a*b*c) : (P 1 1 1 ≥ 0 ∧ P 1 1 0 ≥ 0 ∧ P 1 0 0 ≥ 0) ↔ (∀ a b c : ℝ, a ≥ 0 ∧ b ≥ 0 ∧ c ≥ 0 → P a b c ≥ 0)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph