Prove2Me

Six pairwise linear factors bound a squared triple product

Proved
WorkbookSource.base_30727

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

lean-workbooksource-checked

Prove that (a+b)(b+c)(a+c)(a+b−c)(b+c−a)(a+c−b)≤8a2b2c2(a+b)(b+c)(a+c)(a+b-c)(b+c-a)(a+c-b)\leq 8a^2b^2c^2 if a,b,c>0a,b,c>0.

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_30727 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (a + b) * (b + c) * (c + a) * (a + b - c) * (b + c - a) * (c + a - b) ≤ 8 * a ^ 2 * b ^ 2 * c ^ 2  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_30727; Apache-2.0

View graph