lean_workbook_plus_73843

Proved

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

Let $a^{2}c=x, b^{2}a=y , c^{2}b=z$ So We need to prove that $x^{2}+y^{2}+z^{2}\ge xy+yz +zx$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73843 (a b c x y z : ℝ) (h1 : a^2 * c = x) (h2 : b^2 * a = y) (h3 : c^2 * b = z) : x^2 + y^2 + z^2 ≥ x * y + y * z + z * x   :=  by sorry

Source

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

View graph