lean_workbook_plus_15314

Proved

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

For real a,b prove that $a^6+3a^4b^2+8b^6\ge 2a^3b^3+2a^2b^4+8ab^5$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15314 (a b : ℝ) : a ^ 6 + 3 * a ^ 4 * b ^ 2 + 8 * b ^ 6 ≥ 2 * a ^ 3 * b ^ 3 + 2 * a ^ 2 * b ^ 4 + 8 * a * b ^ 5   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph