lean_workbook_plus_74429

Proved

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

Let $a = \frac {x}{y}, b = \frac {y}{z}, c = \frac {z}{x}$ . Then we can rewrite $(1)$ as \n $\sum_{cyc} \frac {1}{\sqrt {\frac {y}{z} + \frac {y}{x} + \frac {1}{2}}} = \sum_{cyc} \sqrt {\frac {2xz}{2xy + 2yz + xz} }$ \n

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74429  (x y z : ℝ)
  (h₀ : 0 < x ∧ 0 < y ∧ 0 < z)
  (h₁ : x ≠ y)
  (h₂ : y ≠ z)
  (h₃ : z ≠ x) :
  1 / Real.sqrt ((y / z) + (y / x) + 1 / 2) + 1 / Real.sqrt ((z / x) + (z / y) + 1 / 2) + 1 / Real.sqrt ((x / y) + (x / z) + 1 / 2) =
  Real.sqrt (2 * x * z / (2 * x * y + 2 * y * z + x * z)) + Real.sqrt (2 * y * x / (2 * y * z + 2 * z * x + y * x)) + Real.sqrt (2 * z * y / (2 * z * x + 2 * x * y + z * y))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph