Prove2Me

lean_workbook_plus_53978

Proved

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

Find all minimum possible value \n ∣  a−1∣+∣  b−2∣+∣  c−3∣+∣3a+2b+c∣\lvert\;a-1 \rvert+\lvert\;b-2\rvert + \lvert\;c-3\rvert + \lvert3a+2b+c\rvert where a,b,c∈Ra,b,c \in R .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53978 (a b c: ℝ) : 10 / 3 ≤ |a - 1| + |b - 2| + |c - 3| + |3 * a + 2 * b + c|   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph