lean_workbook_plus_60125

Proved

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

Let $a,b,c$ be real numbers such that $a^2 = 2b + 1$ and $b^2 = 2c + 1 .$ Prove that $a+b+c\geq -\frac{3}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60125 (a b c : ℝ) (ha : a^2 = 2 * b + 1) (hb : b^2 = 2 * c + 1) : a + b + c ≥ -3 / 2   :=  by sorry

Source