Prove2Me

lean_workbook_plus_61608

Proved

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

Prove that 12−(a+b)(1−ab)(1+a2)(1+b2)=12(ab+b+a−1)2(1+a2)(1+b2)≥0\frac{1}{2}-\frac{(a+b)(1-ab)}{(1+a^2)(1+b^2)}=\frac{1}{2}\frac{(ab+b+a-1)^2}{(1+a^2)(1+b^2)}\geq0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61608 : ∀ a b : ℝ, (1 / 2 - (a + b) * (1 - a * b) / ((1 + a ^ 2) * (1 + b ^ 2))) = 1 / 2 * (a * b + b + a - 1) ^ 2 / ((1 + a ^ 2) * (1 + b ^ 2)) ∧ (1 / 2 * (a * b + b + a - 1) ^ 2 / ((1 + a ^ 2) * (1 + b ^ 2))) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph