Prove2Me

lean_workbook_plus_1523

Proved

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

This can be expanded to \n 13a2+10b2+5c2=4ab+12bc+6ac13a^2+10b^2+5c^2=4ab+12bc+6ac \n or \n (2a−b)2+(3b−2c)2+(3a−c)2=0 (2a-b)^2+(3b-2c)^2+(3a-c)^2=0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1523 (a b c : ℝ) : 13 * a ^ 2 + 10 * b ^ 2 + 5 * c ^ 2 = 4 * a * b + 12 * b * c + 6 * a * c ↔ (2 * a - b) ^ 2 + (3 * b - 2 * c) ^ 2 + (3 * a - c) ^ 2 = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph