Prove2Me

lean_workbook_plus_57955

Disproved

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

My solution is to use Cauchy-Schwarz on: (x+y+1)2+(y+z+1)2+(z+x+1)2≥13(2x+2y+2z+3)2>13(2x+2y+2z+2)2=43(x+y+z+1)2(x+y+1)^2 + (y+z+1)^2 + (z+x+1)^2 \ge \dfrac{1}{3} (2x+2y+2z+3)^2 > \dfrac{1}{3} (2x+2y+2z+2)^2 = \dfrac{4}{3} (x+y+z+1)^2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57955 : ∀ x y z : ℝ, (x + y + 1) ^ 2 + (y + z + 1) ^ 2 + (z + x + 1) ^ 2 ≥ (4 / 3) * (x + y + z + 1) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph