Prove2Me

lean_workbook_plus_62965

Proved

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

Find the minimum value of S=∣x+1∣+∣x+5∣+∣x+14∣+∣x+97∣+∣x+1920∣S=\left | x+1 \right |+\left | x+5 \right |+\left | x+14 \right |+\left | x+97 \right |+\left | x+1920 \right |

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62965 (x : ℝ) : 2011 ≤ abs (x + 1) + abs (x + 5) + abs (x + 14) + abs (x + 97) + abs (x + 1920)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph