lean_workbook_plus_45475

Proved

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

Let $a,b>0$ and $\frac{ a^3}{b}+\frac{ 2b }{a}=3 .$ Prove that\n\n

a^2+ab+b^2\leq 3

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45475 (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a * b = 1) (h : a^3 / b + 2 * b / a = 3) : a^2 + a * b + b^2 ≤ 3   :=  by sorry

Source

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

View graph