Six mixed sextic monomials bound three cubic products

Proved

WorkbookSource.base_43507

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

lean-workbooksource-checked

Then the ineq. turns into $p^4q^2+q^4p^2+p^4r^2+r^4p^2+q^4r^2+r^4q^2 \ge 2(p^3q^3+q^3r^3+r^3p^3)$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_43507 (p q r : ℝ) : p ^ 4 * q ^ 2 + q ^ 4 * p ^ 2 + p ^ 4 * r ^ 2 + r ^ 4 * p ^ 2 + q ^ 4 * r ^ 2 + r ^ 4 * q ^ 2 ≥ 2 * (p ^ 3 * q ^ 3 + q ^ 3 * r ^ 3 + r ^ 3 * p ^ 3)  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_43507; Apache-2.0

View graph