Prove2Me

lean_workbook_plus_36019

Proved

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

Let a,ba,b be positive real numbers. Prove that:\n

1a+1b+ka+b≥3(1+k4)(12a+b+12b+a)\frac{1}{a}+\frac{1}{b}+\frac{k}{a+b} \ge 3\left(1+\frac{k}{4}\right)\left( \frac{1}{2a+b}+\frac{1}{2b+a}\right)

Where 0≤k≤320\le k\le 32

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_36019 (a b k : ℝ) (ha : 0 < a) (hb : 0 < b) (hk : 0 ≤ k ∧ k ≤ 32) : 1 / a + 1 / b + k / (a + b) ≥ 3 * (1 + k / 4) * (1 / (2 * a + b) + 1 / (2 * b + a))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph