A product of three quadratic factors bounds two squared sums

Proved

WorkbookSource.base_8086

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

lean-workbooksource-checked

Then we have $(a^{2}+2)(b^{2}+2)(c^{2}+2)\geq (a+b+c)^{2}+(ab+bc+ca)^{2}$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_8086 (a b c : ℝ) : (a^2 + 2) * (b^2 + 2) * (c^2 + 2) ≥ (a + b + c)^2 + (a * b + b * c + c * a)^2  :=  by sorry

Source