lean_workbook_plus_53786

Disproved

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

WLOG let $a\ge b\ge c$ . Then we have to show that $a^2 + b^2 + c^2\ge\sqrt 3(a^2 - c^2)$ , which is equivalent to $b^2 + (\sqrt 3 + 1)c^2\ge (\sqrt 3 - 1)a^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53786 :
  ∀ a b c : ℝ, a ≥ b ∧ b ≥ c → a^2 + b^2 + c^2 ≥ Real.sqrt 3 * (a^2 - c^2)   :=  by sorry

Source

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

View graph