lean_workbook_plus_48673
Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Prove that (b+1)(c+1)a2+(c+1)(a+1)b2+(a+1)(b+1)c2+(a+1)(b+1)(c+1)2abc≥1
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48673 : ∀ a b c : ℝ, (a^2 / (b + 1) / (c + 1) + b^2 / (c + 1) / (a + 1) + c^2 / (a + 1) / (b + 1) + 2 * a * b * c / (a + 1) / (b + 1) / (c + 1)) ≥ 1 := by sorry
View graph