lean_workbook_plus_42169

Disproved

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

If $a,b,c \in [1,2]$ then prove that : \n\n

(a+5b+9c) \cdot \left ( \frac{1}{a} + \frac{5}{b} + \frac{9}{c} \right ) \le 225

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42169 : ∀ a b c : ℝ, a ∈ Set.Icc 1 2 ∧ b ∈ Set.Icc 1 2 ∧ c ∈ Set.Icc 1 2 → (a + 5 * b + 9 * c) * (1 / a + 5 / b + 9 / c) ≤ 225   :=  by sorry

Source

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

View graph