Prove2Me

lean_workbook_plus_65997

Disproved

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

Prove that ab+bc+caa+b=aba+b+c≤a+b4+c\frac{ab+bc+ca}{a+b}=\frac{ab}{a+b} +c\le \frac{a+b}{4}+c

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

View graph