Prove2Me

lean_workbook_plus_8050

Proved

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

Find xx such that 32+42−2×3×4x=52+62−2×5×6(−x)3^2 + 4^2 - 2\times3\times4x = 5^2 + 6^2 - 2\times5\times6(-x).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8050 (x : ℝ) : (3^2 + 4^2 - 2*3*4*x = 5^2 + 6^2 - 2*5*6*(-x)) ↔ x = -3/7   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph