Prove2Me

lean_workbook_plus_37439

Proved

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

Another solution ab=9ab = 9 a+b=12a+b = 12 (a+b)2=a2+2ab+b2(a+b)^2 = a^2 + 2ab + b^2 (a−b)2=a2−2ab+b2(a-b)^2 = a^2 - 2ab + b^2 So, (a−b)2=(a+b)2−4ab=144−4∗9=108(a-b)^2 = (a+b)^2 - 4ab = 144 - 4*9 = 108 ∣a−b∣=63|a-b| = \boxed{6\sqrt3}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37439  (a b : ℝ)
  (h₀ : a * b = 9)
  (h₁ : a + b = 12) :
  |a - b| = 6 * Real.sqrt 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph