Prove2Me

lean_workbook_plus_8750

Proved

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

Suppose a+b=1 where a and b are positive numbers. (i) Show that ab≤14ab\leq\frac14 . (ii) Find the minimum value of (a+1a)(b+1b)\left(a+\frac1a\right)\left(b+\frac1b\right) .

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

View graph