lean_workbook_plus_52841

Disproved

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

For k=1,we have: $\frac{(a+b)^2}{c^2+ab}+ \frac{(b+c)^2}{a^2+bc}+ \frac{(c+a)^2}{b^2+ca} \ge 6$ (Darij grinberg)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52841 :
  ∀ a b c : ℝ,
    (a + b) ^ 2 / (c ^ 2 + a * b) + (b + c) ^ 2 / (a ^ 2 + b * c) + (c + a) ^ 2 / (b ^ 2 + c * a) ≥
      6   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph