Prove2Me

lean_workbook_plus_49215

Disproved

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

Prove that:\na2−b2a2+bc+b2−c2b2+ca+c2−a2c2+ab≤0\frac{a^{2}-b^{2}}{a^{2}+bc}+\frac{b^{2}-c^{2}}{b^{2}+ca}+\frac{c^{2}-a^{2}}{c^{2}+ab}\le 0

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

View graph