lean_workbook_plus_3010

Proved

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

Prove that if positive real numbers $a, b, c$ satisfies $a+b+c=3$ then $\sqrt{3} \leq \sqrt{a^2+b^2+c^2}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3010 : ∀ a b c : ℝ, a + b + c = 3 → Real.sqrt 3 ≤ Real.sqrt (a ^ 2 + b ^ 2 + c ^ 2)   :=  by sorry

Source