lean_workbook_plus_81296

Proved

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

Let $x,y,z$ be nonnegative integers that sum to $6$ . Find the maximum value of $xy^2z^3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81296 (x y z : ℕ) (hx : x + y + z = 6) : x * y^2 * z^3 ≤ 108   :=  by sorry

Source