lean_workbook_plus_1478

Proved

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

If $a=b=c=2$ so $\sum_{cyc}\frac{(a-1)^2}{a^2+2}=\frac{1}{2}$ . We'll prove that $\frac{1}{2}$ is the answer.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1478 (a b c : ℝ) (ha : a = 2) (hb : b = 2) (hc : c = 2) : (a - 1) ^ 2 / (a ^ 2 + 2) + (b - 1) ^ 2 / (b ^ 2 + 2) + (c - 1) ^ 2 / (c ^ 2 + 2) = 1 / 2   :=  by sorry

Source

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

View graph