Prove2Me

lean_workbook_plus_64764

Disproved

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

We have cos⁡a2+cos⁡b2+cos⁡c2+2cos⁡acos⁡bcos⁡c=1\cos{a}^2+\cos{b}^2+\cos{c}^2+2\cos{a}\cos{b}\cos{c}=1 . Let cos⁡a=xy(y+z)(x+z)\cos{a}=\sqrt{\frac{xy}{(y+z)(x+z)}} . The inequality becomes 1+4xyz(x+y)(y+z)(z+x)≤xy(y+z)(x+z)+zy(y+x)(x+z)+xz(y+z)(x+y)1+4\frac{xyz}{(x+y)(y+z)(z+x)}\le \sqrt{\frac{xy}{(y+z)(x+z)}}+\sqrt{\frac{zy}{(y+x)(x+z)}}+\sqrt{\frac{xz}{(y+z)(x+y)}}

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

View graph