Prove2Me

lean_workbook_plus_37058

Proved

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

Let a,b,c>0.a,b,c> 0 . Prove that

1ab+c+12+1bc+a+14+1ca+b+12≥165\dfrac{1}{\dfrac{a}{b+c}+\dfrac{1}{ 2}}+\dfrac{1}{\dfrac{b}{c+a}+\dfrac{1}{4}}+\dfrac{1}{\dfrac{c}{a+b}+\dfrac{1}{ 2}}\geq \dfrac{16}{5}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37058 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (1 / (a / (b + c) + 1 / 2) + 1 / (b / (c + a) + 1 / 4) + 1 / (c / (a + b) + 1 / 2)) ≥ 16 / 5   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph