lean_workbook_plus_11665

Disproved

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

Prove that $LHS=\frac{(a+b+c)^2}{2(ab+bc+ca)}-\frac{1}{2}\left[\frac{a^2+b^2+c^2}{ab+bc+ca}+\frac{8abc}{(a+b)(b+c)(c+a)}-2\right] \le \frac{(a+b+c)^2}{2(ab+bc+ca)}=RHS$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11665 : ∀ a b c : ℝ, a * b * c > 0 → (a + b + c) ^ 2 / (2 * (a * b + b * c + c * a)) - 1 / 2 * ((a ^ 2 + b ^ 2 + c ^ 2) / (a * b + b * c + c * a) + 8 * a * b * c / ((a + b) * (b + c) * (c + a)) - 2) ≤ (a + b + c) ^ 2 / (2 * (a * b + b * c + c * a))   :=  by sorry

Source

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

View graph