lean_workbook_plus_40007

Proved

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

Prove that for all real numbers $x$ ,\n\n $|x|+x^2+||x|-1|+6|x-2|+|x^2-1|+3|2x+1|\ge 17$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40007 (x : ℝ) : abs x + x ^ 2 + abs (abs x - 1) + 6 * abs (x - 2) + abs (x ^ 2 - 1) + 3 * abs (2 * x + 1) ≥ 17   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph