lean_workbook_plus_77372

Proved

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

Prove the inequality: $\frac{1}{a^2}+\frac{1}{b^2}+\frac{1}{c^2} \geq \frac{1}{ab}+\frac{1}{bc}+\frac{1}{ca}$ , where $a^2 = \sqrt{x+y}$ , $b^2 = \sqrt{y+z}$ , and $c^2 = \sqrt{x+z}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77372 (x y z a b c : ℝ) (ha : a^2 = Real.sqrt (x + y)) (hb : b^2 = Real.sqrt (y + z)) (hc : c^2 = Real.sqrt (x + z)) : 1 / a^2 + 1 / b^2 + 1 / c^2 ≥ 1 / (a * b) + 1 / (b * c) + 1 / (c * a)   :=  by sorry

Source

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

View graph