lean_workbook_plus_19151

Proved

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

Prove that for positive reals $a$ , $b$ , $c$ with $abc=1$ , the inequality $(a^2+1)(b^2+1)(c^2+1) \geq (a+1)(b+1)(c+1)$ holds.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19151 (a b c : ℝ) (habc : a * b * c = 1) :
  (a^2 + 1) * (b^2 + 1) * (c^2 + 1) ≥ (a + 1) * (b + 1) * (c + 1)   :=  by sorry

Source

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

View graph