lean_workbook_plus_67407

Proved

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

We have given three positive real numbers $a,b,c$ satisfying the equation\n\n $(1) \;\; (a + c)(b^2 + ac) = 4a$ .\n\nEquation (1) is equivalent\n\n $(2) \;\; ca^2 + (b^2 + c^2 - 4)a + b^2c = 0$ .\n\nEquation (1) is a second degree equation in $a$ which is solvable iff its discriminant $D \geq 0$ , i.e.\n\n $D = (b^2 + c^2 - 4)^2 - (2bc)^2 \geq 0$ ,\n\nyielding\n\n $(3) \;\; |b^2 + c^2 - 4| \geq 2bc$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67407  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : (a + c) * (b^2 + a * c) = 4 * a) :
  abs (b^2 + c^2 - 4) ≥ 2 * b * c   :=  by sorry

Source

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

View graph