Prove2Me

lean_workbook_plus_81139

Disproved

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

Prove that\n\n

a2+b2+c2+ab+bc+ca+1a2+b2+c2+2ab+bc+ca≤a(b+c+1)a2+2bc+b(c+a+1)b2+2ca+c(a+b+1)c2+2ab≤a(a+b+1)+b(b+c+1)+c(c+a+1)ab+bc+ca\frac{a^2+b^2+c^2+ab+bc+ca+1}{a^2+b^2+c^2}+\frac{2}{ab+bc+ca} \leq \frac{a(b+c+1)}{a^2+2bc}+\frac{b(c+a+1)}{b^2+2ca}+\frac{c(a+b+1)}{c^2+2ab} \leq \frac{a(a+b+1)+b(b+c+1)+c(c+a+1)}{ab+bc+ca}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_81139 : ∀ a b c : ℝ, (a^2 + b^2 + c^2 + a * b + b * c + c * a + 1) / (a^2 + b^2 + c^2) + 2 / (a * b + b * c + c * a) ≤ a * (b + c + 1) / (a^2 + 2 * b * c) + b * (c + a + 1) / (b^2 + 2 * c * a) + c * (a + b + 1) / (c^2 + 2 * a * b) ∧ a * (b + c + 1) / (a^2 + 2 * b * c) + b * (c + a + 1) / (b^2 + 2 * c * a) + c * (a + b + 1) / (c^2 + 2 * a * b) ≤ (a * (a + b + 1) + b * (b + c + 1) + c * (c + a + 1)) / (a * b + b * c + c * a)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph