Prove2Me

Three quadratic factors bound three squared pairwise sums

Proved
WorkbookSource.plus_17927

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

lean-workbooksource-checked

∏(2a2+b2+c2)=∏[(a2+b2)+(a2+c2)]≥∏[(a+b)22+(a+c)22]≥∏(a+b)2(a+c)2=(a+b)2(b+c)2(c+a)2\prod (2a^{2}+b^{2}+c^{2})=\prod [(a^{2}+b^{2})+(a^{2}+c^{2})]\geq \prod [\frac{(a+b)^{2}}{2}+\frac{(a+c)^{2}}{2}]\geq \prod \sqrt{(a+b)^{2}(a+c)^{2}}=(a+b)^{2}(b+c)^{2}(c+a)^{2}

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.plus_17927 (a b c : ℝ) : (2 * a ^ 2 + b ^ 2 + c ^ 2) * (2 * b ^ 2 + c ^ 2 + a ^ 2) * (2 * c ^ 2 + a ^ 2 + b ^ 2) ≥ (a + b) ^ 2 * (b + c) ^ 2 * (c + a) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_17927; Apache-2.0

View graph