Prove2Me

An eighth-degree three-variable polynomial is nonnegative

Proved
WorkbookSource.base_1361

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that P=a6b2+2 a6bc+a6c2−2 a5b3−2 a5b2c−2 a5bc2−2 a5c3+2 a4b4+4 a4b2c2+2 a4c4−2 a3b5−2 a3b3c2−2 a3b2c3−2 a3c5+a2b6−2 a2b5c+4 a2b4c2−2 a2b3c3+4 a2b2c4−2 a2bc5+a2c6+2 ab6c−2 ab5c2−2 ab2c5+2 abc6+b6c2−2 b5c3+2 b4c4−2 b3c5+b2c6≥0 P={a}^{6}{b}^{2}+2\,{a}^{6}bc+{a}^{6}{c}^{2}-2\,{a}^{5}{b}^{3}-2\,{a}^{5}{b}^{2}c-2\,{a}^{5}b{c}^{2}-2\,{a}^{5}{c}^{3}+2\,{a}^{4}{b}^{4}+4\,{a}^{4}{b}^{2}{c}^{2}+2\,{a}^{4}{c}^{4}-2\,{a}^{3}{b}^{5}-2\,{a}^{3}{b}^{3}{c}^{2}-2\,{a}^{3}{b}^{2}{c}^{3}-2\,{a}^{3}{c}^{5}+{a}^{2}{b}^{6}-2\,{a}^{2}{b}^{5}c+4\,{a}^{2}{b}^{4}{c}^{2}-2\,{a}^{2}{b}^{3}{c}^{3}+4\,{a}^{2}{b}^{2}{c}^{4}-2\,{a}^{2}b{c}^{5}+{a}^{2}{c}^{6}+2\,a{b}^{6}c-2\,a{b}^{5}{c}^{2}-2\,a{b}^{2}{c}^{5}+2\,ab{c}^{6}+{b}^{6}{c}^{2}-2\,{b}^{5}{c}^{3}+2\,{b}^{4}{c}^{4}-2\,{b}^{3}{c}^{5}+{b}^{2}{c}^{6} \geq 0

Source: InternLM Lean-Workbook, record lean_workbook_1361 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_1361 (a b c : ℝ) : a^6 * b^2 + 2 * a^6 * b * c + a^6 * c^2 - 2 * a^5 * b^3 - 2 * a^5 * b^2 * c - 2 * a^5 * b * c^2 - 2 * a^5 * c^3 + 2 * a^4 * b^4 + 4 * a^4 * b^2 * c^2 + 2 * a^4 * c^4 - 2 * a^3 * b^5 - 2 * a^3 * b^3 * c^2 - 2 * a^3 * b^2 * c^3 - 2 * a^3 * c^5 + a^2 * b^6 - 2 * a^2 * b^5 * c + 4 * a^2 * b^4 * c^2 - 2 * a^2 * b^3 * c^3 + 4 * a^2 * b^2 * c^4 - 2 * a^2 * b * c^5 + a^2 * c^6 + 2 * a * b^6 * c - 2 * a * b^5 * c^2 - 2 * a * b^2 * c^5 + 2 * a * b * c^6 + b^6 * c^2 - 2 * b^5 * c^3 + 2 * b^4 * c^4 - 2 * b^3 * c^5 + b^2 * c^6 ≥ 0  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_1361; Apache-2.0

View graph