Prove2Me

lean_workbook_plus_52843

Disproved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

It is also equivalent to the following: \n \n (1b+1c+1a)((a−b)2b+(b−c)2c+(c−a)2a) \left(\frac {1}{b} + \frac {1}{c} + \frac {1}{a}\right)\left(\frac {(a - b)^2}{b} + \frac {(b - c)^2}{c} + \frac {(c - a)^2}{a}\right) ≥(a−bb+b−cc+c−aa)2 \ge \left(\frac {a - b}{b} + \frac {b - c}{c} + \frac {c - a}{a}\right)^2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52843 :
  ∀ a b c : ℝ, (1 / b + 1 / c + 1 / a) * ((a - b) ^ 2 / b + (b - c) ^ 2 / c + (c - a) ^ 2 / a) ≥ ((a - b) / b + (b - c) / c + (c - a) / a) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph