lean_workbook_plus_78621

Proved

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

Let $t_1,t_2>0$ ,prove that: $(t_2+1)^2(t_1+1)^2(1+t_1^2)(1+t_2^2)\geq 4(t_1+t_2)^2(1+t_1t_2)^2.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78621 (t1 t2 : ℝ) (ht1 : 0 < t1) (ht2 : 0 < t2) : (t2 + 1) ^ 2 * (t1 + 1) ^ 2 * (1 + t1 ^ 2) * (1 + t2 ^ 2) ≥ 4 * (t1 + t2) ^ 2 * (1 + t1 * t2) ^ 2   :=  by sorry

Source

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

View graph