Prove2Me

lean_workbook_plus_2022

Proved

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

Given the condition a+b+c≥abca + b + c \geq abc, prove the inequality (u+v+w)2≥3(uv+vw+uw)(u + v + w)^2 \geq 3(uv + vw + uw), where u=1a,v=1b,w=1cu = \frac{1}{a}, v = \frac{1}{b}, w = \frac{1}{c}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2022 (a b c u v w : ℝ) (h : a + b + c ≥ a * b * c) : (u + v + w) ^ 2 ≥ 3 * (u * v + v * w + w * u)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph