Prove2Me

lean_workbook_plus_69409

Proved

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

Let a,b,c>1a,b,c>1 and (a−1)(b−1)(c−1)=63−10.(a-1)(b-1)(c-1)=6 \sqrt{3} -10. Prove that \n\n

a+b+c≤abca+b+c\leq abc
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69409 (a b c : ℝ) (ha : 1 < a) (hb : 1 < b) (hc : 1 < c) (habc : a * b * c = 1) (h : (a - 1) * (b - 1) * (c - 1) = 6 * Real.sqrt 3 - 10) : a + b + c ≤ a * b * c   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph