Prove2Me

lean_workbook_plus_3931

Proved

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

For 0<a,b,c,d<10<a,b,c,d<1 . Prove that: (1−a)(1−b)(1−c)(1−d)>1−a−b−c−d(1-a)(1-b)(1-c)(1-d)>1-a-b-c-d .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3931 (a b c d : ℝ) (habc : 0 < a ∧ a < 1) (hbd : 0 < b ∧ b < 1) (hcd : 0 < c ∧ c < 1) (hded : 0 < d ∧ d < 1): (1-a)*(1-b)*(1-c)*(1-d) > 1-a-b-c-d   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph