lean_workbook_plus_65220

Proved

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

$(a^6+1)/2+(a^6+2)/3+(a^6+5)/6\ge 2a^3/2+3a^2/3+6a/6=a^3+a^2+a$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65220 (a : ℝ) : (a^6 + 1) / 2 + (a^6 + 2) / 3 + (a^6 + 5) / 6 ≥ a^3 + a^2 + a   :=  by sorry

Source