Prove2Me

lean_workbook_plus_75005

Proved

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

Let a,b,c≥0a,b,c\ge0 , abc=1,abc=1 , prove or disprove that (1+a2)(1+b2)(1+c2)≥(1+a)(1+b)(1+c).(1+a^2)(1+b^2)(1+c^2)\ge(1+a)(1+b)(1+c).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75005 (a b c : ℝ) (h1 : a ≥ 0 ∧ b ≥ 0 ∧ c ≥ 0 ∧ a * b * c = 1) :
  (1 + a ^ 2) * (1 + b ^ 2) * (1 + c ^ 2) ≥ (1 + a) * (1 + b) * (1 + c)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph