A weighted quadratic lower bound at unit sum

Proved

WorkbookSource.base_1598

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

lean-workbooksource-checked

Let $x, y, z$ be reals such that $x+y+z=1.$ Prove that $2x^2 + 3y^2 + 4z^2\geq \frac{12}{13}$ .

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_1598 (x y z : ℝ) (h : x + y + z = 1) : 2*x^2 + 3*y^2 + 4*z^2 ≥ 12/13  :=  by sorry

Source