lean_workbook_plus_4939

Disproved

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

And $(1+t^2_1)(1+t^2_2)\geq (t_1t_2+1)^2\geq (t_1+t_2)(t_1t_2+1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4939 : ∀ t1 t2 : ℝ, (1 + t1 ^ 2) * (1 + t2 ^ 2) ≥ (t1 * t2 + 1) ^ 2 ∧ (t1 * t2 + 1) ^ 2 ≥ (t1 + t2) * (t1 * t2 + 1)   :=  by sorry

Source

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

View graph