A mixed product bound under linked quadratic relations

Proved

WorkbookSource.plus_2302

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let $a,b,c$ be real numbers such that $a^2+b=4$ and $b^2+c=8 .$ Prove that

2ab+ bc+ ca \geq-32

Source: InternLM Lean-Workbook, record lean_workbook_plus_2302 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_2302 (a b c : ℝ) (h₁ : a^2 + b = 4) (h₂ : b^2 + c = 8) : 2 * a * b + b * c + c * a ≥ -32   :=  by sorry

Source