lean_workbook_plus_35491

Proved

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

Let $x = \frac{a}{b}; y = \frac{b}{c}; z = \frac{c}{a}$ We are asked to prove that $a^2+b^2+c^2 \ge ab+bc+ca$ \nwhich is true as $\frac{1}{2}(\sum (a-b)^2) \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35491  (a b c : ℝ)
  (x y z : ℝ)
  (h₀ : x = a / b)
  (h₁ : y = b / c)
  (h₂ : z = c / a) :
  a^2 + b^2 + c^2 ≥ a * b + b * c + c * a   :=  by sorry

Source

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

View graph