lean_workbook_plus_57647

Disproved

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

$= (a-b)^2(\frac{c}{2}-\frac{1}{2}-\frac{c}{a+b+\sqrt{2(a^2+b^2)}}) \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57647 : ∀ a b c : ℝ, (a - b) ^ 2 * (c / 2 - 1 / 2 - c / (a + b + Real.sqrt (2 * (a ^ 2 + b ^ 2)))) ≥ 0   :=  by sorry

Source