lean_workbook_plus_72931

Disproved

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

$\Rightarrow \frac{1}{1+a}\geq \frac{2\sqrt{bc}}{\sqrt{(1+b)(1+c)}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72931 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → 1 / (1 + a) ≥ 2 * Real.sqrt (b * c) / Real.sqrt ((1 + b) * (1 + c))   :=  by sorry

Source

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

View graph