Prove2Me

lean_workbook_plus_68938

Disproved

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

A weaker inequality proven by the student:\n

ab+c+bc+a+ca+b+25(ab+bc+ca)(a+b+c)2≥52≈7.071\frac{a}{b+c} + \frac{b}{c+a} +\frac{c}{a+b} + \frac{25(ab+bc+ca)}{(a+b+c)^2} \geq 5\sqrt{2} \approx 7.071
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68938 : ∀ a b c : ℝ, (a / (b + c) + b / (c + a) + c / (a + b) + (25 * (a * b + b * c + c * a)) / (a + b + c) ^ 2) ≥ 5 * Real.sqrt 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph