← Formalpedia
lean_workbook_plus_47112 Disproved by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
2 , a 2 + b 2 + c 2 a b + b c + c a ≥ 2 3 ( a b + c + b c + a + c a + b ) . 2, \dfrac{a^2+b^2+c^2}{ab+bc+ca}\geq \dfrac{2}{3}(\dfrac{a}{b+c}+\dfrac{b}{c+a}+\dfrac{c}{a+b}). 2 , ab + b c + c a a 2 + b 2 + c 2 ≥ 3 2 ( b + c a + c + a b + a + b c ) . ⟺ \iff ⟺ a 2 + b 2 + c 2 a b + b c + c a + 2 ≥ 2 3 ( a b + c + 1 + b c + a + 1 + c a + b + 1 ) . \dfrac{a^2+b^2+c^2}{ab+bc+ca}+2\geq \dfrac{2}{3}(\dfrac{a}{b+c}+1+\dfrac{b}{c+a}+1+\dfrac{c}{a+b}+1). ab + b c + c a a 2 + b 2 + c 2 + 2 ≥ 3 2 ( b + c a + 1 + c + a b + 1 + a + b c + 1 ) . ⟺ \iff ⟺ ( a + b + c ) 2 a b + b c + c a ≥ 2 3 ( a + b + c b + c + a + b + c c + a + a + b + c a + b ) . \dfrac{(a+b+c)^2}{ab+bc+ca}\geq \dfrac{2}{3}(\dfrac{a+b+c}{b+c}+\dfrac{a+b+c}{c+a}+\dfrac{a+b+c}{a+b}). ab + b c + c a ( a + b + c ) 2 ≥ 3 2 ( b + c a + b + c + c + a a + b + c + a + b a + b + c ) . ⟺ \iff ⟺ a + b + c a b + b c + c a ≥ 2 3 ( 1 b + c + 1 c + a + 1 a + b ) . \dfrac{a+b+c}{ab+bc+ca}\geq \dfrac{2}{3}(\dfrac{1}{b+c}+\dfrac{1}{c+a}+\dfrac{1}{a+b}). ab + b c + c a a + b + c ≥ 3 2 ( b + c 1 + c + a 1 + a + b 1 ) .
Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_47112 : ∀ a b c : ℝ, (a^2 + b^2 + c^2) / (a * b + b * c + c * a) + 2 ≥ (2 / 3) * (a / (b + c) + b / (c + a) + c / (a + b)) := by sorry View graph