lean_workbook_plus_1689

Proved

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

Let $a,b$ and $c$ be real numbers such that $a^2+b^2+c^2=1.$ Prove that

(a-b)^2+(b-c)^2+(c-a)^2\le3

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1689 : ∀ a b c : ℝ, a^2 + b^2 + c^2 = 1 → (a - b)^2 + (b - c)^2 + (c - a)^2 ≤ 3   :=  by sorry

Source