lean_workbook_plus_30791

Proved

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

Let $a$ and $b$ are non-negative real numbers. Prove that: $(a^{2}+2005b+2006)(b^{2}+2005a+2006)\geq(2007a+2005)(2007b+2005).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30791 (a b : ℝ) (ha : a ≥ 0) (hb : b ≥ 0) : (a^2 + 2005*b + 2006)*(b^2 + 2005*a + 2006) ≥ (2007*a + 2005)*(2007*b + 2005)   :=  by sorry

Source

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

View graph