lean_workbook_plus_74491

Disproved

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

$\frac {{a\left( {a - b} \right)\left( {a - c} \right)}}{{a^2 + 2bc}} + \frac {{b\left( {b - a} \right)\left( {b - c} \right)}}{{b^2 + 2ca}} = \frac {{\left( {a - b} \right)^2 \left( {2a^2 c + 2b^2 c + abc - ac^2 - bc^2 } \right)}}{{\left( {a^2 + 2bc} \right)\left( {b^2 + 2ca} \right)}} \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74491 :
  ∀ a b c : ℝ,
    (a * (a - b) * (a - c)) / (a^2 + 2 * b * c) + (b * (b - a) * (b - c)) / (b^2 + 2 * c * a) =
      (a - b)^2 * (2 * a^2 * c + 2 * b^2 * c + a * b * c - a * c^2 - b * c^2) / ((a^2 + 2 * b * c) * (b^2 + 2 * c * a)) ∧
    (a - b)^2 * (2 * a^2 * c + 2 * b^2 * c + a * b * c - a * c^2 - b * c^2) / ((a^2 + 2 * b * c) * (b^2 + 2 * c * a)) ≥ 0   :=  by sorry

Source

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

View graph