lean_workbook_plus_40344

Proved

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

Let $a,b,c$ be real numbers such that $a+b+c=0$ and $|a|+|b|+|c|=1$ . Prove that $a+\frac{b}{2}+\frac{c}{3}\le \frac{1}{3}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40344 (a b c : ℝ) (hab : a + b + c = 0) (hbc : abs a + abs b + abs c = 1) :
  a + b / 2 + c / 3 ≤ 1 / 3   :=  by sorry

Source