Prove2Me

lean_workbook_plus_56829

Proved

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

Let a,b,c>0a,b,c > 0 such that ab+bc+ca+abc≥4ab + bc + ca + abc \ge 4 . Prove that \n a+b+c≥3+(b−c)2b+c+4a + b + c \ge 3 + \frac{{{{\left( {b - c} \right)}^2}}}{{b + c + 4}} \nFrom condition we get a=4−bcb+c+bc,a = \frac{4-bc}{b+c+bc}, so we will show that \n 4−bcb+c+bc+b+c⩾3+(b−c)2b+c+4,\frac{4-bc}{b+c+bc} + b + c \geqslant 3 + \frac{{{{\left( {b - c} \right)}^2}}}{{b + c + 4}}, or \n (2bc+b+c−4)2(bc+b+c)(b+c+4)⩾0.\frac{(2bc+b+c-4)^2}{(bc+b+c)(b+c+4)} \geqslant 0. Done.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_56829  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : a * b + b * c + c * a + a * b * c ≥ 4) :
  a + b + c ≥ 3 + (b - c)^2 / (b + c + 4)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph