lean_workbook_plus_22649

Proved

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

Prove that for any real numbers $a$ and $b$ the following inequality holds: \n $\left( a^{2}+1\right) \left( b^{2}+1\right) +50\geq2\left( 2a+1\right)\left( 3b+1\right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_22649 (a b: ℝ) :  (a^2 + 1) * (b^2 + 1) + 50 ≥ 2 * (2 * a + 1) * (3 * b + 1)   :=  by sorry

Source

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

View graph