Prove2Me

Two bounds for a shifted three-factor product

Proved
WorkbookSource.problem_32102

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

lean-workbooksource-checked

Prove that for non-negative real numbers x,y,zx, y, z with x+y+z=1x + y + z = 1, the following inequality holds: 8≤(x+1)(y+2)(z+3)≤128 \leq (x + 1)(y + 2)(z + 3) \leq 12

Source: InternLM Lean-Workbook, record lean_workbook_32102 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_32102 (x y z : ℝ) (hx : x + y + z = 1) (hx' : 0 ≤ x ∧ 0 ≤ y ∧ 0 ≤ z) : 8 ≤ (x + 1) * (y + 2) * (z + 3) ∧ (x + 1) * (y + 2) * (z + 3) ≤ 12  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_32102; Apache-2.0

View graph