lean_workbook_plus_75045

Disproved

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

It would suffice to prove that: \n $\sqrt{a+1}+\sqrt{b+1}+\sqrt{c+1}+\sqrt{d+1}\ge \sqrt{ab+1}+\sqrt{bc+1}+\sqrt{cd+1}+\sqrt{ad+1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75045 : ∀ a b c d : ℝ, (Real.sqrt (a + 1) + Real.sqrt (b + 1) + Real.sqrt (c + 1) + Real.sqrt (d + 1)) ≥ (Real.sqrt (a * b + 1) + Real.sqrt (b * c + 1) + Real.sqrt (c * d + 1) + Real.sqrt (a * d + 1))   :=  by sorry

Source

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

View graph