Prove2Me

lean_workbook_plus_63575

Proved

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

Prove that for all real numbers a,b,c,da,b,c,d, (abc+acd+abd+bcd−a−b−c−d)2+(abcd−ab−ac−ad−bc−bd−cd+1)2≥1(abc+acd+abd+bcd-a-b-c-d)^2 +(abcd-ab-ac-ad-bc-bd-cd+1)^2 \geq 1.

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

View graph