Prove2Me

The quadratic sum bounds shifted cyclic ratios at fixed sum three

Proved
WorkbookSource.plus_70607

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

lean-workbooksource-checked

Let a,b,c∈R+a,b,c \in \mathbb{R}^+ such that a+b+c=3a+b+c=3 Prove that a2+b2+c2≥2+a2+b+2+b2+c+2+c2+aa^2+b^2+c^2 \geq \frac{2+a}{2+b}+\frac{2+b}{2+c}+\frac{2+c}{2+a}

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

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

View graph