Prove2Me

lean_workbook_plus_59597

Proved

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

We have sure a≥2,b≥3,c≥4a\ge 2,b\ge 3,c\ge 4 , thus (1+1a)(2+1b)(3+1c)≤(1+12)(2+13)(3+14)=918\left( 1+\frac{1}{a} \right)\left( 2+\frac{1}{b} \right)\left( 3+\frac{1}{c} \right)\le \left( 1+\frac{1}{2} \right)\left( 2+\frac{1}{3} \right)\left( 3+\frac{1}{4} \right)=\frac{91}{8}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59597 (a b c : ℝ) (ha : 2 ≤ a) (hb : 3 ≤ b) (hc : 4 ≤ c) : (1 + 1 / a) * (2 + 1 / b) * (3 + 1 / c) ≤ 91 / 8   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph