Prove2Me

lean_workbook_plus_68207

Proved

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

Let a,b,ca,b,c be reals.Then \n\n

(a2+1)(b2+1)(c2+1)⩾(a+b)(b+c)(c+a)+13(ab+bc+ca−a−b−c)2(a^2+1)(b^2+1)(c^2+1)\geqslant (a+b)(b+c)(c+a) +\frac{1}{3} (ab+bc+ca-a-b-c)^2
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68207 (a b c : ℝ) : (a^2 + 1) * (b^2 + 1) * (c^2 + 1) ≥ (a + b) * (b + c) * (c + a) + (1 / 3) * (a * b + b * c + c * a - a - b - c)^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph