Prove2Me

A strict square-sum bound at sum one half

Proved
WorkbookSource.problem_24926

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

lean-workbooksource-checked

take a=x+y a=x+y , b=y+z b=y+z and c=z+x c=z+x , x,y,z>0 x,y,z>0 and x+y+z=12 x+y+z=\frac{1}2 . So, your inequalitie is transformed into (x+y)2+(y+z)2+(z+x)2<12 (x+y)^{2}+(y+z)^{2}+(z+x)^{2}<\frac{1}2 2x2+2y2+2z2+2xy+2yz+2zx=x2+y2+z2+(x+y+z)2<12 2x^{2}+2y^{2}+2z^{2}+2xy+2yz+2zx=x^{2}+y^{2}+z^{2}+(x+y+z)^{2}<\frac{1}2 So, it's equivalent to x2+y2+z2<14 x^{2}+y^{2}+z^{2}<\frac{1}4 Using the fact that for positive numbers x2+y2<(x+y)2 x^{2}+y^{2}<(x+y)^{2} we have the desired result.

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_24926  (x y z : ℝ)
  (h₀ : 0 < x ∧ 0 < y ∧ 0 < z)
  (h₁ : x + y + z = 1 / 2) :
  x^2 + y^2 + z^2 < 1 / 4  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_24926; Apache-2.0

View graph