lean_workbook_plus_49123

Proved

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

Prove that: $1/(a-b)^2+1/(b-c)^2+1/(c-a)^2=(1/(a-b)+1/(b-c)+1/(c-a))^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49123 {a b c : ℝ} (hab : a ≠ b) (hbc : b ≠ c) (hca : c ≠ a) : 1 / (a - b) ^ 2 + 1 / (b - c) ^ 2 + 1 / (c - a) ^ 2 = (1 / (a - b) + 1 / (b - c) + 1 / (c - a)) ^ 2   :=  by sorry

Source

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

View graph