Prove2Me

lean_workbook_plus_38510

Disproved

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

Prove the inequality\n\na2+(1−b)2+b2(1−c)2+c2+(1−a)2≥322 \sqrt {a^2 + (1 - b)^2} + \sqrt { b^2 (1 - c)^2} + \sqrt {c^2 + (1 - a)^2} \ge \frac { 3 \sqrt {2}}{2}\n\nholds for arbitrary real numbers a,b,c a,b,c

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38510 : ∀ a b c : ℝ, (Real.sqrt (a ^ 2 + (1 - b) ^ 2) + Real.sqrt (b ^ 2 * (1 - c) ^ 2) + Real.sqrt (c ^ 2 + (1 - a) ^ 2)) ≥ (3 * Real.sqrt 2) / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph