Prove2Me

lean_workbook_plus_13465

Proved

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

If x2+y2+z2=k(xy+xz+yz)x^2+y^2+z^2=k(xy+xz+yz) and k≥1k\geq1, prove that 3(k+1)3≥8(k+2)3(k+1)^3\geq8(k+2).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13465 (x y z : ℝ) (k : ℝ) (h₁ : k ≥ 1) (h₂ : x^2 + y^2 + z^2 = k * (x * y + x * z + y * z)) : 3 * (k + 1)^3 ≥ 8 * (k + 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph