lean_workbook_plus_21575

Proved

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

Let $a,b,c> 1$ three distinct natural numbers , prove that $(1+\frac{1}{a})(2+\frac{1}{b})(3+\frac{1}{c})\leq\frac{91}{8}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21575 (a b c : ℕ) (hab : a ≠ b) (hbc : b ≠ c) (hca : c ≠ a) (ha : 1 < a) (hb : 1 < b) (hc : 1 < c) : (1 + 1 / a) * (2 + 1 / b) * (3 + 1 / c) ≤ 91 / 8   :=  by sorry

Source

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

View graph