Prove2Me

lean_workbook_plus_69971

Proved

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

Let a,ba,b be positive real numbers such that k(a+b)=1+ab.k(a+b)=1+ab. a+b+1a+1b≥4k.a+b+\frac{1}{a}+\frac{1}{b}\geq 4k. Where k≥1.k\geq 1.

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

View graph