A product of shifted quadratic ratios is at least 2744 over 27

Proved

WorkbookSource.base_12020

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

lean-workbooksource-checked

x,y,z>0

$\left( 8/3+{\frac {3\,{x}^{2}+yz}{{y}^{2}+{z}^{2}}} \right) \left( 8/3+{\frac {3\,{y}^{2}+zx}{{x}^{2}+{z}^{2}}} \right) \left( 8/3+{\frac {3\,{z}^{2}+xy}{{y}^{2}+{x}^{2}}} \right) \geq {\frac {2744}{27}}$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_12020 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (8 / 3 + (3 * x ^ 2 + y * z) / (y ^ 2 + z ^ 2)) * (8 / 3 + (3 * y ^ 2 + z * x) / (z ^ 2 + x ^ 2)) * (8 / 3 + (3 * z ^ 2 + x * y) / (x ^ 2 + y ^ 2)) ≥ 2744 / 27  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_12020; Apache-2.0

View graph