lean_workbook_plus_3968

Proved

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

Let $a, b, c > 0$ . Prove that: \n

(a+b)(b+c)(c+a) \geqslant \dfrac{2abc(a+b+c+1)^2}{ab+bc+ca+1}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3968 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (a+b)*(b+c)*(c+a) ≥ (2*a*b*c*(a+b+c+1)^2)/(a*b+b*c+c*a+1)   :=  by sorry

Source

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

View graph