A product of quadratic expressions under unit sum

Proved

WorkbookCorrected.base_49865

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-formalizationlean-workbooksource-checked

Prove $54a^{2}b^{2}\leq 4(a^{2}b^{2}+a^{2}+b^{2})(a^{2}+b^{2}+1)$ , where $a,b$ are positive reals and $a+b=1$ .

Source: InternLM Lean-Workbook, record lean_workbook_49865 (Apache-2.0). Natural-language proposition preserved; missing source domain assumptions restored. Proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookCorrected.base_49865 (a b : ℝ) (source_domain_a : 0 < a) (source_domain_b : 0 < b) (h : a + b = 1) : 54 * a ^ 2 * b ^ 2 ≤ 4 * (a ^ 2 * b ^ 2 + a ^ 2 + b ^ 2) * (a ^ 2 + b ^ 2 + 1)  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_49865; Apache-2.0

View graph